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

chore: fix test output

Browse source
This commit is contained in:
Leonardo de Moura 2020-12-21 07:34:10 -08:00
parent 82f87ddd5b
commit 856559a983
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/pplevel.lean.expected.out
View file

@ -1,6 +1,6 @@
Type (max u v w) : Type ((max u v w) + 1)
Type u : Type (u + 1)
id.{max u v w} : {α : Sort (max u v w)} → α → α
Monad.{max u v, w + 1} : (Type (max u v) → Type (w + 1)) → Type (max (w + 1) ((max u v) + 1))
Monad.{max u v, w + 1} : (Type (max u v) → Type (w + 1)) → Type (max ((max u v) + 1) (w + 1))
Type (max (u + 1) w (v + 2)) : Type ((max (u + 1) w (v + 2)) + 1)
Type u_1 : Type (u_1 + 1)