aniva/Pantograph
aniva
/
Pantograph
1
1
Fork 0
Code Issues 10 Pull Requests 1 Packages Projects Releases 1 Wiki Activity

feat: Add definitions and theorems to the environment #41

Merged
aniva merged 9 commits from env/add-decl into dev 2023-12-26 12:41:02 -08:00
Conversation 0 Commits 9 Files Changed 10 +5 -5
2 changed files with 5 additions and 5 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files
Showing only changes of commit 77232d5a1e - Show all commits

6
Test/Catalog.lean → Test/Environment.lean
View File

@ -2,7 +2,7 @@ import LSpec
import Pantograph.Serial import Pantograph.Serial
import Pantograph.Environment import Pantograph.Environment
namespace Pantograph.Test.Catalog namespace Pantograph.Test.Environment
open Pantograph open Pantograph
open Lean open Lean
@ -24,7 +24,7 @@ def suite: IO LSpec.TestSeq := do
(opts := {}) (opts := {})
(trustLevel := 1) (trustLevel := 1)
return LSpec.group "Catalog" $ return LSpec.group "Environment" $
(LSpec.group "Symbol visibility" (← test_symbol_visibility env)) (LSpec.group "Symbol visibility" (← test_symbol_visibility env))
end Pantograph.Test.Catalog end Pantograph.Test.Environment

4
Test/Main.lean
View File

@ -1,5 +1,5 @@
import LSpec import LSpec
import Test.Catalog import Test.Environment
import Test.Holes import Test.Holes
import Test.Integration import Test.Integration
import Test.Proofs import Test.Proofs
@ -15,7 +15,7 @@ def main := do
Integration.suite, Integration.suite,
Proofs.suite, Proofs.suite,
Serial.suite, Serial.suite,
Catalog.suite Environment.suite
] ]
let all ← suites.foldlM (λ acc m => do pure $ acc ++ (← m)) LSpec.TestSeq.done let all ← suites.foldlM (λ acc m => do pure $ acc ++ (← m)) LSpec.TestSeq.done
LSpec.lspecIO $ all LSpec.lspecIO $ all