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

test: old frontend exports at new frontend

Browse source 
We can now "see" exports made in the old frontend in the new one.

cc @dselsam @kha
This commit is contained in:
Leonardo de Moura 2020-01-11 13:49:42 -08:00
parent 3e233b6f3d
commit 6762f8ea9a
1 changed files with 3 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
tests/lean/run/newfrontend1.lean
View file

@ -27,9 +27,11 @@ set_option pp.all true
#check foo 1
#check foo 3 (c := Bool.false)
#check foo 3 (c := false)
def Nat.boo (a : Nat) :=
succ a -- succ here is resolved as `Nat.succ`.
#check Nat.boo
#check true