4
let f = λx : ℕ. x + 1 in f : ℕ → ℕ
4
let f = (λx. x + 1) : ℕ → ℕ in f : ℕ → ℕ
let f = λx. x + 1 : ℕ in f : ℕ → ℕ
let f = λx. x + 1 : ℕ in f : ℕ → ℕ
(9, 8)
5
λx : ℤ, y : ℕ. x * y : ℤ → ℕ → ℤ
[false, true, true]
let f = λg : ℤ → ℕ → Bool. [g(1)(1), g(1)(2), g(-1)(0)] in f(λx, y : ℤ. x + 1 == y) : List(Bool)
3
TAbs_ Lam () (<[PWild_ ()]> TNat_ () 3)
3