proof relevant parse 2

Author: awalterschulze

Katydid/Conal/Calculus.lean

@@ -11,12 +11,8 @@ open String
 -- Print Parse
 -- set_option pp.all true
 open List
-def a_or_b := (char 'a' ⋃ char 'b')
-#print a_or_b
-def a_or_b_parse_a := a_or_b (toList "a")
--- #eval a_or_b_parse_a
 
-def p : a_or_b (toList "a") -> Nat := by
+def example_of_proof_relevant_parse : (char 'a' ⋃ char 'b') (toList "a") -> Nat := by
   intro x
   cases x with
   | inl xa =>
@@ -30,6 +26,31 @@ def p : a_or_b (toList "a") -> Nat := by
     | mk eq =>
       contradiction
 
+def example_of_proof_relevant_parse2 : (char 'a', (char 'b' ⋃ char 'c')) (toList "ab") -> Nat := by
+  intro x1
+  simp at x1
+  cases x1 with
+  | mk x1 x2 =>
+    cases x2 with
+    | mk x2 x3 =>
+      cases x3 with
+      | mk x3 x4 =>
+        cases x3 with
+        | mk x3 =>
+          cases x4 with
+          | mk x4 x5 =>
+            cases x4 with
+            | inl x4 =>
+                cases x4 with
+                | mk x4 =>
+                  subst_vars
+                  exact 0
+            | inr x4 =>
+              cases x4 with
+              | mk x4 =>
+                subst_vars
+                contradiction
+
 -- ν⇃ : Lang → Set ℓ      -- “nullable”
 -- ν⇃ P = P []
 def ν (P : Lang α) : Type u := -- backslash nu