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

fix(tests/lean/run/new_compiler): broken test

Browse source
This commit is contained in:
Leonardo de Moura 2019-08-16 09:46:44 -07:00
parent dae30a4ea6
commit 9d37f53d83
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/new_compiler.lean
View file

@ -41,8 +41,10 @@ def add' : Nat → Nat → Nat
def aux (i : Nat) (h : i > 0) :=
i
axiom bad (α : Sort u) : α
unsafe def foo2 : Nat :=
@False.rec (fun _ => Nat) sorry
@False.rec (fun _ => Nat) (bad _)
set_option pp.notation false