35 lines
666 B
Text
35 lines
666 B
Text
Prop
|
||
Type
|
||
Type
|
||
Type 1
|
||
Type _
|
||
Type (_+2)
|
||
Nat
|
||
List Nat
|
||
id Nat
|
||
id (id (id Nat))
|
||
List Nat
|
||
@id Type Nat
|
||
List.{0} Nat
|
||
id.{2} Nat
|
||
id (@id Type Nat)
|
||
fun (a : Nat) => a
|
||
fun (a b : Nat) => a
|
||
fun (a : Nat)(b : Bool) => a
|
||
fun {a b : Nat} => a
|
||
typeAs ({α : Type} → α → α) fun {α : Type}(a : α) => a
|
||
fun {α : Type}[_inst_1 : HasToString α](a : α) => @HasToString.toString α _inst_1 a
|
||
(α : Type) → α
|
||
(α β : Type) → α
|
||
Type → Type → Type
|
||
(α : Type) → α → α
|
||
(α : Type) → (a : α) → Eq a a
|
||
{α : Type} → α
|
||
{α : Type} → [_inst_1 : HasToString α] → α
|
||
0
|
||
1
|
||
42
|
||
"hi"
|
||
(Prod.mk 1 2).fst
|
||
or (HasLess.Less 1 2) Bool.true
|
||
id (fun (a : Nat) => a) 0
|