a3cb39eac9
This PR migrates most remaining tests to the new test suite. It also completes the migration of directories like `tests/lean/run`, meaning that PRs trying to add tests to those old directories will now fail.
15 lines
476 B
Text
15 lines
476 B
Text
inductive HList {α : Type v} (β : α → Type u) : List α → Type (max u v)
|
||
| nil : HList β []
|
||
| cons : β i → HList β is → HList β (i::is)
|
||
|
||
infix:67 " :: " => HList.cons
|
||
|
||
inductive Member : α → List α → Type
|
||
| head : Member a (a::as)
|
||
| tail : Member a bs → Member a (b::bs)
|
||
|
||
def HList.get : HList β is → Member i is → β i
|
||
| a::as, .head => a
|
||
--v textDocument/hover
|
||
| a::as, .tail h => as.get h
|
||
--^ textDocument/hover
|