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
1:13:
  |
1 | :parse \x, y. x
  |             ^
Anonymous functions (lambdas) can only have a single argument.
Instead of \x, y. ... you can write  \x. \y. ...
https://disco-lang.readthedocs.io/en/latest/reference/anonymous-func.html