michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

fix(tests/lean): avoid 'sorry' in expected output

Browse source
This commit is contained in:
Leonardo de Moura 2014-11-06 14:06:55 -08:00
parent af88e34588
commit 4fa363adbf
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
tests/lean/error_full_names.lean
View file

@ -1,4 +1,4 @@
import data.nat
import data.nat.basic
namespace foo
open nat
inductive nat : Type := zero, foosucc : nat → nat