From 0002f111f94d53f9ebdc769a31c3a2f4388f2aa6 Mon Sep 17 00:00:00 2001
From: Walter Schulze <awalterschulze@gmail.com>
Date: Sun, 25 Feb 2024 15:37:44 +0000
Subject: [PATCH] trfl function

---
 Katydid/Conal/Examples.lean | 16 ++++++++++++++--
 Katydid/Std/Tipe2.lean      |  4 ++--
 2 files changed, 16 insertions(+), 4 deletions(-)

diff --git a/Katydid/Conal/Examples.lean b/Katydid/Conal/Examples.lean
index 9ea33a6..2c6104d 100644
--- a/Katydid/Conal/Examples.lean
+++ b/Katydid/Conal/Examples.lean
@@ -27,8 +27,20 @@ example : (char 'a' ⋃ char 'b') (String.toList "b") := by
 
 -- _ : a⋆b ('a' ∷ 'b' ∷ [])
 -- _ = ([ 'a' ] , [ 'b' ]) , refl , refl , refl
-example : (char 'a', char 'b') (String.toList "ab") := by sorry
-  -- TODO: ⟨ ['a'], ['b'], TEq.mk rfl, TEq.mk rfl, rfl ⟩
+example : (char 'a', char 'b') (String.toList "ab") := by
+  simp
+  exists ['a']
+  exists ['b']
+  exists trfl
+  exists trfl
+
+example : (char 'a', char 'b') (String.toList "ab") := by
+  simp
+  refine PSigma.mk ['a'] ?a
+  refine PSigma.mk ['b'] ?b
+  refine PSigma.mk trfl ?c
+  refine PSigma.mk trfl ?d
+  rfl
 
 example : ((char 'a')*) (String.toList "a") := by sorry
   -- TODO:
diff --git a/Katydid/Std/Tipe2.lean b/Katydid/Std/Tipe2.lean
index b488c5d..c6808f8 100644
--- a/Katydid/Std/Tipe2.lean
+++ b/Katydid/Std/Tipe2.lean
@@ -12,8 +12,8 @@ example : TEq 1 1 := by
   constructor
   rfl
 
--- @[match_pattern] def trfl {α : Type u} {a : α} : TEq a a := @TEq.refl α a
--- attribute [simp] trfl
+@[match_pattern] def trfl {α : Type u} {a : α} : TEq a a := TEq.mk rfl
+attribute [simp] trfl
 
 -- the abbreviation ≡ is typed with `slash = =`
 infixl:65 " ≡ " => TEq