move Tipe to Conal folder

katydid · Aug 27, 2024 · 796a88c · 796a88c
1 parent d0c62b3
commit 796a88c
Show file tree

Hide file tree

Showing 5 changed files with 4 additions and 4 deletions.
diff --git a/Katydid.lean b/Katydid.lean
@@ -1,6 +1,5 @@
 import Katydid.Std.Ordering
 import Katydid.Std.OrderingThunk
-import Katydid.Std.Tipe
 import Katydid.Std.Lists
 import Katydid.Std.Ltac
 import Katydid.Std.Balistic
@@ -10,6 +9,7 @@ import Katydid.Example.SimpLibrary
 import Katydid.Expr.Desc
 import Katydid.Expr.Regex
 
+import Katydid.Conal.Tipe
 import Katydid.Conal.Decidability
 import Katydid.Conal.Function
 import Katydid.Conal.Language

diff --git a/Katydid/Conal/Calculus.lean b/Katydid/Conal/Calculus.lean
@@ -1,7 +1,7 @@
 -- A translation to Lean from Agda
 -- https://github.com/conal/paper-2021-language-derivatives/blob/main/Calculus.lagda
 
-import Katydid.Std.Tipe
+import Katydid.Conal.Tipe
 import Katydid.Conal.Function
 import Katydid.Conal.Language
 

diff --git a/Katydid/Conal/Function.lean b/Katydid/Conal/Function.lean
@@ -1,6 +1,6 @@
 -- An approximation of the Function module in the Agda standard library.
 
-import Katydid.Std.Tipe
+import Katydid.Conal.Tipe
 import Mathlib.Logic.Equiv.Defs
 
 -- A ↔ B = Inverse A B

diff --git a/Katydid/Conal/Language.lean b/Katydid/Conal/Language.lean
@@ -1,7 +1,7 @@
 -- A translation to Lean from Agda
 -- https://github.com/conal/paper-2021-language-derivatives/blob/main/Language.lagda
 
-import Katydid.Std.Tipe
+import Katydid.Conal.Tipe
 
 namespace Language
 

diff --git a/Katydid/Std/Tipe.lean → Katydid/Conal/Tipe.lean b/Katydid/Std/Tipe.lean → Katydid/Conal/Tipe.lean