refactor: Rename {Serial,Delate}.lean
This commit is contained in:
parent
8fe4c78c2a
commit
1c4f38e5eb
|
@ -4,5 +4,5 @@ import Pantograph.Frontend
|
||||||
import Pantograph.Goal
|
import Pantograph.Goal
|
||||||
import Pantograph.Library
|
import Pantograph.Library
|
||||||
import Pantograph.Protocol
|
import Pantograph.Protocol
|
||||||
import Pantograph.Serial
|
import Pantograph.Delate
|
||||||
import Pantograph.Version
|
import Pantograph.Version
|
||||||
|
|
|
@ -1,5 +1,5 @@
|
||||||
import Pantograph.Protocol
|
import Pantograph.Protocol
|
||||||
import Pantograph.Serial
|
import Pantograph.Delate
|
||||||
import Lean
|
import Lean
|
||||||
|
|
||||||
open Lean
|
open Lean
|
||||||
|
|
|
@ -2,7 +2,7 @@ import Pantograph.Condensed
|
||||||
import Pantograph.Environment
|
import Pantograph.Environment
|
||||||
import Pantograph.Goal
|
import Pantograph.Goal
|
||||||
import Pantograph.Protocol
|
import Pantograph.Protocol
|
||||||
import Pantograph.Serial
|
import Pantograph.Delate
|
||||||
import Pantograph.Version
|
import Pantograph.Version
|
||||||
import Lean
|
import Lean
|
||||||
|
|
||||||
|
|
|
@ -1,10 +1,10 @@
|
||||||
import LSpec
|
import LSpec
|
||||||
import Pantograph.Serial
|
import Pantograph.Delate
|
||||||
import Test.Common
|
import Test.Common
|
||||||
import Lean
|
import Lean
|
||||||
|
|
||||||
open Lean
|
open Lean
|
||||||
namespace Pantograph.Test.Serial
|
namespace Pantograph.Test.Delate
|
||||||
|
|
||||||
open Pantograph
|
open Pantograph
|
||||||
|
|
||||||
|
@ -106,4 +106,4 @@ def suite (env: Environment): List (String × IO LSpec.TestSeq) :=
|
||||||
("Instance", test_instance env),
|
("Instance", test_instance env),
|
||||||
]
|
]
|
||||||
|
|
||||||
end Pantograph.Test.Serial
|
end Pantograph.Test.Delate
|
|
@ -1,5 +1,5 @@
|
||||||
import LSpec
|
import LSpec
|
||||||
import Pantograph.Serial
|
import Pantograph.Delate
|
||||||
import Pantograph.Environment
|
import Pantograph.Environment
|
||||||
import Test.Common
|
import Test.Common
|
||||||
import Lean
|
import Lean
|
||||||
|
|
|
@ -5,7 +5,7 @@ import Test.Integration
|
||||||
import Test.Library
|
import Test.Library
|
||||||
import Test.Metavar
|
import Test.Metavar
|
||||||
import Test.Proofs
|
import Test.Proofs
|
||||||
import Test.Serial
|
import Test.Delate
|
||||||
import Test.Tactic
|
import Test.Tactic
|
||||||
|
|
||||||
-- Test running infrastructure
|
-- Test running infrastructure
|
||||||
|
@ -50,7 +50,7 @@ def main (args: List String) := do
|
||||||
("Library", Library.suite env_default),
|
("Library", Library.suite env_default),
|
||||||
("Metavar", Metavar.suite env_default),
|
("Metavar", Metavar.suite env_default),
|
||||||
("Proofs", Proofs.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/Congruence", Tactic.Congruence.suite env_default),
|
||||||
("Tactic/Motivated Apply", Tactic.MotivatedApply.suite env_default),
|
("Tactic/Motivated Apply", Tactic.MotivatedApply.suite env_default),
|
||||||
("Tactic/No Confuse", Tactic.NoConfuse.suite env_default),
|
("Tactic/No Confuse", Tactic.NoConfuse.suite env_default),
|
||||||
|
|
|
@ -1,6 +1,6 @@
|
||||||
import LSpec
|
import LSpec
|
||||||
import Pantograph.Goal
|
import Pantograph.Goal
|
||||||
import Pantograph.Serial
|
import Pantograph.Delate
|
||||||
import Test.Common
|
import Test.Common
|
||||||
import Lean
|
import Lean
|
||||||
|
|
||||||
|
|
|
@ -3,7 +3,7 @@ Tests pertaining to goals with no interdependencies
|
||||||
-/
|
-/
|
||||||
import LSpec
|
import LSpec
|
||||||
import Pantograph.Goal
|
import Pantograph.Goal
|
||||||
import Pantograph.Serial
|
import Pantograph.Delate
|
||||||
import Test.Common
|
import Test.Common
|
||||||
|
|
||||||
namespace Pantograph.Test.Proofs
|
namespace Pantograph.Test.Proofs
|
||||||
|
|
Loading…
Reference in New Issue