max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: restore disabled tests

Browse source
This commit is contained in:
Leonardo de Moura 2020-01-08 21:24:01 -08:00
parent c06d515027
commit 65370e9322
2 changed files with 3 additions and 7 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
tests/lean/run/frontend1.lean
View file

@ -216,10 +216,9 @@ def three := 3
#eval run "#check g (z := three)"
#eval run "#check g three (z := zero)"
-- TODO fix test
-- #eval run "open Lean.Parser
-- @[termParser] def myParser : Lean.Parser.Parser Lean.ParserKind.leading := parser! coe \"hi\"
-- #check myParser"
#eval run "open Lean.Parser
@[termParser] def myParser : Lean.Parser.Parser Lean.ParserKind.leading := parser! coe \"hi\"
#check myParser"
#eval run "#check (fun stx => if True then let e := stx; HasPure.pure e else HasPure.pure stx : Nat → Id Nat)"
#eval run "constant n : Nat #check n"

3
tests/lean/run/termParserAttr.lean
View file

@ -24,9 +24,6 @@ ParserDescr.node `boo
open Lean.Elab.Term
-- TODO fix test
#exit
@[termElab tst] def elabTst : TermElab :=
fun stx expected? =>
elabTerm (stx.getArg 1) expected?