Functions on Dependent Functions

Stream: general

[Devon Tuma]

Are there special rules for functions operating on dependent functions? I'm not sure why one of these works but the other doesn't:

def test₁ : (Π {i : unit}, ℕ) → (Π {i : unit}, ℕ) :=
id -- works

def test₂ : (Π {i : unit}, ℕ) → (Π {i : unit}, ℕ) :=
λ x, x -- fails

[Yaël Dillies]

This is because of the {} binders.

[Reid Barton]

It has to do with the implicitness of i. In the second argument, i gets filled in (somehow) and then you're left with a number, not a function.

[Reid Barton]

If you don't want i to get filled in automatically in this situation, you can use the {{ }} or \{{ \}} binders (e.g. docs#function.injective)