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

chore: more general type universes in example

Browse source
This commit is contained in:
Leonardo de Moura 2022-03-15 05:18:27 -07:00
parent 7ee7ca30b8
commit aa68057c85
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/run/deBruijn.lean
View file

@ -1,4 +1,4 @@
inductive HList {α : Type u} (β : α → Type u) : List α → Type u
inductive HList {α : Type v} (β : α → Type u) : List α → Type (max u v)
| nil : HList β []
| cons : β i → HList β is → HList β (i::is)