now build all files again

Katydid.lean

@@ -7,6 +7,9 @@ import Katydid.Std.Balistic
 
 import Katydid.Example.SimpLibrary
 
+import Katydid.Expr.Desc
+import Katydid.Expr.Regex
+
 import Katydid.Conal.Language
 import Katydid.Conal.LanguageNotation
 import Katydid.Conal.Calculus

Katydid/Expr/Desc.lean

@@ -1,12 +1,13 @@
-import Std.Data.List.Lemmas
-import Std.Classes.Order
+import Katydid.Std.Lists
 
 /-
 We want to represent some nested function calls for a very restricted language, for example:
   and(lt(3, 5), contains("abcd", "bc"))
 We represent the description (including AST) of the expr, or as we call it the Descriptor here:
 -/
 
+namespace Desc
+
 inductive Desc where
   | intro
     (name: String)
@@ -227,5 +228,7 @@ theorem cmp_symm : ∀ (x y : SmartDesc),
   -- TODO
   sorry
 
-instance : Std.OrientedCmp SmartDesc.compare where
+instance : Batteries.OrientedCmp SmartDesc.compare where
   symm x y := cmp_symm x y
+
+end Desc

Katydid/Expr/Regex.lean

@@ -1,6 +1,8 @@
 import Lean
 open List
 
+namespace Regex
+
 inductive Regex : Type where
   | emptyset : Regex
   | emptystr : Regex
@@ -53,56 +55,58 @@ partial def elabRegex : Lean.Syntax → Lean.Meta.MetaM Lean.Expr
 
 elab " {{ " e:regex " }} " : term => elabRegex e
 
-#check {{ ∅ }}
+example: Regex := {{ ∅ }}
+
+example: Regex := {{ 'a' }}
 
-#check {{ 'a' }}
+example: Regex := {{ a }}
 
-#check {{ a }}
+example: Regex := {{ abc }}
 
-#check {{ abc }}
+example: Regex := {{ 'a''b''c' }}
 
-#check {{ 'a''b''c' }}
+example: Regex := {{ "" }}
 
-#eval {{ "" }}
+example: Regex := {{ a }}
 
-#eval {{ a }}
+example: Regex := {{ "a" }}
 
-#eval {{ "a" }}
+example: Regex := {{ ab }}
 
-#eval {{ ab }}
+example: Regex := {{ "ab" }}
 
-#eval {{ "ab" }}
+example: Regex := {{ abc }}
 
-#eval {{ abc }}
+example: Regex := {{ "abc" }}
 
-#eval {{ "abc" }}
+example: Regex := {{ abc }}
 
-#check {{ abc }}
+example: Regex := {{ "abc" }}
 
-#check {{ "abc" }}
+example: Regex := {{ ε }}
 
-#check {{ ε }}
+example: Regex := {{ 'a' }}
 
-#eval {{ 'a' }}
+example: Regex := {{ a }}
 
-#check {{ a }}
+example: Regex := {{ 'a' | 'b' }}
 
-#check {{ 'a' | 'b' }}
+example: Regex := {{ ab }}
 
-#check {{ ab }}
+example: Regex := {{ a b }}
 
-#check {{ a b }}
+example: Regex := {{ a b c }}
 
-#check {{ a b c }}
+example: Regex := {{ a* }}
 
-#eval {{ a* }}
+example: Regex := {{ (a)* }}
 
-#eval {{ (a)* }}
+example: Regex := {{ "a"* }}
 
-#eval {{ "a"* }}
+example: Regex := {{ ("a")* }}
 
-#eval {{ ("a")* }}
+example: Regex := {{ (a)(b) }}
 
-#eval {{ (a)(b) }}
+example: Regex := {{ (a | b)* }}
 
-#eval {{ (a | b)* }}
+end Regex