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

chore(tests/lean/inductive_resultant_level_inferrence): update expected output

Browse source
This commit is contained in:
Daniel Selsam 2017-03-11 18:41:37 -08:00 • committed by Leonardo de Moura
parent d37fd17725
commit 89d0f1773e
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/inductive_resultant_level_inference.lean.expected.out
View file

@ -18,7 +18,7 @@ X5.foo.{u} : Sort u → Sort (max 1 u)
X6.foo.{u} : Sort u → Type (u+2)
7. ?U unifies with a max: error
inductive_resultant_level_inference.lean:82:0: error: resultant level unifies with complex level 'max u_2 u_1', provide the universe levels explicitly
inductive_resultant_level_inference.lean:82:0: error: resultant level unifies with complex level 'max u_1 u_2', provide the universe levels explicitly
8. wrapping inductive returns element in different universe: error
inductive_resultant_level_inference.lean:92:0: error: nested occurrence 'X8.bar.{(max 1 v)} foo' lives in universe 'succ (max 1 v)' but must live in resultant universe 'max 1 v'