Pantograph/Test/Library.lean

39 lines
1.3 KiB
Plaintext
Raw Permalink Blame History

This file contains ambiguous Unicode characters

This file contains Unicode characters that might be confused with other characters. If you think that this is intentional, you can safely ignore this warning. Use the Escape button to reveal them.

import LSpec
import Lean
import Pantograph.Library
import Test.Common
open Lean
open Pantograph
namespace Pantograph.Test.Library
def test_expr_echo (env: Environment): IO LSpec.TestSeq := do
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" }
}))
let echoResult ← exprEcho prop_and_proof (expectedType? := .some "Σ' p:Prop, p") (options := { printExprAST := true })
let tests := tests.append (LSpec.test "fail" (echoResult.toOption == .some {
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)))",
}
}))
return tests
runCoreMSeq env (options := #["pp.proofs.threshold=100"]) inner
def suite (env: Environment): List (String × IO LSpec.TestSeq) :=
[
("expr_echo", test_expr_echo env),
]
end Pantograph.Test.Library