06ad52575a
After this commit, we have to use an explicit `discard` in code such as ``` def g (x : Nat) : IO Nat := ... def f (x : Nat) : IO Unit := do discard <| g x -- type error without the `discard` IO.println x ``` Motivation: prevent users from making mistakes such as ``` def f (xs : Array Nat) : IO Unit := do xs.set! 0 1 IO.println xs ``` when they meant to write ``` def f (xs : Array Nat) : IO Unit := do let xs := xs.set! 0 1 IO.println xs ```
62 lines
837 B
Text
62 lines
837 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
|
||
Sum.{0, 0} Nat 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 :
|
||
ToString α]
|
||
(a : α) =>
|
||
@toString α inst a
|
||
(α : Type) → α
|
||
(α β : Type) → α
|
||
Type → Type → Type
|
||
(α : Type) → α → α
|
||
(α : Type) →
|
||
(a : α) → a = a
|
||
{α : Type} → α
|
||
{α : Type} →
|
||
[inst :
|
||
ToString α] →
|
||
α
|
||
0
|
||
1
|
||
42
|
||
"hi"
|
||
{ type := Nat,
|
||
val := 0 :
|
||
PointedType }
|
||
(1, 2, 3)
|
||
(1, 2).fst
|
||
1 < 2 || true
|
||
id
|
||
(fun (a : Nat) =>
|
||
a)
|
||
0
|
||
typeAs Nat
|
||
(do
|
||
let x ← pure 1
|
||
discard (pure 2)
|
||
let y : Nat := 3
|
||
pure (x + y))
|