diff --git a/Pantograph.lean b/Pantograph.lean index 292efb9..72c4906 100644 --- a/Pantograph.lean +++ b/Pantograph.lean @@ -4,5 +4,5 @@ import Pantograph.Frontend import Pantograph.Goal import Pantograph.Library import Pantograph.Protocol -import Pantograph.Serial +import Pantograph.Delate import Pantograph.Version diff --git a/Pantograph/Serial.lean b/Pantograph/Delate.lean similarity index 100% rename from Pantograph/Serial.lean rename to Pantograph/Delate.lean diff --git a/Pantograph/Environment.lean b/Pantograph/Environment.lean index 040d801..87e3a2f 100644 --- a/Pantograph/Environment.lean +++ b/Pantograph/Environment.lean @@ -1,5 +1,5 @@ import Pantograph.Protocol -import Pantograph.Serial +import Pantograph.Delate import Lean open Lean diff --git a/Pantograph/Library.lean b/Pantograph/Library.lean index 23a2046..8a5db24 100644 --- a/Pantograph/Library.lean +++ b/Pantograph/Library.lean @@ -2,7 +2,7 @@ import Pantograph.Condensed import Pantograph.Environment import Pantograph.Goal import Pantograph.Protocol -import Pantograph.Serial +import Pantograph.Delate import Pantograph.Version import Lean diff --git a/Test/Serial.lean b/Test/Delate.lean similarity index 98% rename from Test/Serial.lean rename to Test/Delate.lean index 1c00501..57411e8 100644 --- a/Test/Serial.lean +++ b/Test/Delate.lean @@ -1,10 +1,10 @@ import LSpec -import Pantograph.Serial +import Pantograph.Delate import Test.Common import Lean open Lean -namespace Pantograph.Test.Serial +namespace Pantograph.Test.Delate open Pantograph @@ -106,4 +106,4 @@ def suite (env: Environment): List (String × IO LSpec.TestSeq) := ("Instance", test_instance env), ] -end Pantograph.Test.Serial +end Pantograph.Test.Delate diff --git a/Test/Environment.lean b/Test/Environment.lean index 6b418f7..79d04ed 100644 --- a/Test/Environment.lean +++ b/Test/Environment.lean @@ -1,5 +1,5 @@ import LSpec -import Pantograph.Serial +import Pantograph.Delate import Pantograph.Environment import Test.Common import Lean diff --git a/Test/Main.lean b/Test/Main.lean index 0fde5fa..25bb0d9 100644 --- a/Test/Main.lean +++ b/Test/Main.lean @@ -5,7 +5,7 @@ import Test.Integration import Test.Library import Test.Metavar import Test.Proofs -import Test.Serial +import Test.Delate import Test.Tactic -- Test running infrastructure @@ -50,7 +50,7 @@ def main (args: List String) := do ("Library", Library.suite env_default), ("Metavar", Metavar.suite env_default), ("Proofs", Proofs.suite env_default), - ("Serial", Serial.suite env_default), + ("Delate", Delate.suite env_default), ("Tactic/Congruence", Tactic.Congruence.suite env_default), ("Tactic/Motivated Apply", Tactic.MotivatedApply.suite env_default), ("Tactic/No Confuse", Tactic.NoConfuse.suite env_default), diff --git a/Test/Metavar.lean b/Test/Metavar.lean index dbaf2cc..84860b3 100644 --- a/Test/Metavar.lean +++ b/Test/Metavar.lean @@ -1,6 +1,6 @@ import LSpec import Pantograph.Goal -import Pantograph.Serial +import Pantograph.Delate import Test.Common import Lean diff --git a/Test/Proofs.lean b/Test/Proofs.lean index 1da21ae..437bb64 100644 --- a/Test/Proofs.lean +++ b/Test/Proofs.lean @@ -3,7 +3,7 @@ Tests pertaining to goals with no interdependencies -/ import LSpec import Pantograph.Goal -import Pantograph.Serial +import Pantograph.Delate import Test.Common namespace Pantograph.Test.Proofs