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

chore(tests/lean/parser1): fix test

Browse source
This commit is contained in:
Leonardo de Moura 2018-05-02 17:37:55 -07:00
parent 48ba4370d5
commit d9101cb950
1 changed files with 0 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
tests/lean/parser1.lean
View file

@ -111,7 +111,6 @@ do cmd ← lean.ir.parse_instr,
#eval test parse_instr_pp "o := cnstr 0 3 0" "o := cnstr 0 3 0"
#eval test parse_instr_pp "set o 0 x" "set o 0 x"
#eval test parse_instr_pp "x := get o 0" "x := get o 0"
#eval test parse_instr_pp "«set» := get o 0" "«set» := get o 0"
#eval test parse_instr_pp "sset o 10 x" "sset o 10 x"
#eval test parse_instr_pp "x : bool := sget o 0" "x : bool := sget o 0"
#eval test parse_instr_pp "x := closure f a" "x := closure f a"