Pantograph/Test/Library.lean

39 lines
1.3 KiB
Plaintext
Raw Permalink Normal View History

2024-03-31 16:43:30 -07:00
import LSpec
import Lean
import Pantograph.Library
import Test.Common
open Lean
open Pantograph
namespace Pantograph.Test.Library
2024-04-06 14:07:13 -07:00
def test_expr_echo (env: Environment): IO LSpec.TestSeq := do
2024-03-31 16:43:30 -07:00
let inner: CoreM LSpec.TestSeq := do
let prop_and_proof := "⟨∀ (x: Prop), x → x, λ (x: Prop) (h: x) => h⟩"
let tests := LSpec.TestSeq.done
let echoResult ← exprEcho prop_and_proof (options := {})
let tests := tests.append (LSpec.test "fail" (echoResult.toOption == .some {
type := { pp? := "?m.2" }, expr := { pp? := "?m.3" }
}))
2024-03-31 17:09:24 -07:00
let echoResult ← exprEcho prop_and_proof (expectedType? := .some "Σ' p:Prop, p") (options := { printExprAST := true })
2024-03-31 16:43:30 -07:00
let tests := tests.append (LSpec.test "fail" (echoResult.toOption == .some {
2024-03-31 17:09:24 -07:00
type := {
pp? := "(p : Prop) ×' p",
sexp? := "((:c PSigma) (:sort 0) (:lambda p (:sort 0) 0))",
},
expr := {
pp? := "⟨∀ (x : Prop), x → x, fun x h => h⟩",
sexp? := "((:c PSigma.mk) (:sort 0) (:lambda p (:sort 0) 0) (:forall x (:sort 0) (:forall _ 0 1)) (:lambda x (:sort 0) (:lambda h 0 0)))",
}
2024-03-31 16:43:30 -07:00
}))
return tests
runCoreMSeq env (options := #["pp.proofs.threshold=100"]) inner
2024-04-06 14:07:13 -07:00
def suite (env: Environment): List (String × IO LSpec.TestSeq) :=
[
("expr_echo", test_expr_echo env),
]
2024-03-31 16:43:30 -07:00
end Pantograph.Test.Library