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

fix(frontends/lean/structure_cmd): bad test output

Browse source
This commit is contained in:
Leonardo de Moura 2014-11-05 12:01:38 -08:00
parent 677e0aeef6
commit f8a2bc41a5
1 changed files with 0 additions and 7 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
tests/lean/bad_structures.lean.expected.out
View file

@ -1,10 +1,3 @@
bad_structures.lean:1:49: error: invalid 'structure', the resultant universe must be provided when explicit universe levels are being used bad_structures.lean:1:49: error: invalid 'structure', the resultant universe must be provided when explicit universe levels are being used
bad_structures.lean:4:49: error: invalid 'structure', the resultant universe must be provided when explicit universe levels are being used bad_structures.lean:4:49: error: invalid 'structure', the resultant universe must be provided when explicit universe levels are being used
bad_structures.lean:7:49: error: invalid 'structure', the resultant universe level should not be zero for any universe parameter assignment bad_structures.lean:7:49: error: invalid 'structure', the resultant universe level should not be zero for any universe parameter assignment
generated type
proj_type: Pi {A : Type.{l}} {B : Type.{l}} (c : prod.{l} A B), A
proj_val: fun {A : Type.{l}} {B : Type.{l}} (c : prod.{l} A B), (prod.rec.{l l} A B (fun (c : prod.{l} A B), A) (fun (pr1 : A) (pr2 : B), pr1) c)
proj_type: Pi {A : Type.{l}} {B : Type.{l}} (c : prod.{l} A B), B
proj_val: fun {A : Type.{l}} {B : Type.{l}} (c : prod.{l} A B), (prod.rec.{l l} A B (fun (c : prod.{l} A B), B) (fun (pr1 : A) (pr2 : B), pr2) c)
generated projs
generated auxiliary