Zulip Chat Archive
Stream: general
Topic: Type check requires id
Patrick Johnson (May 28 2022 at 04:05):
Why does the first example fail, but the second one works? I read somewhere that adding id
s helps type-checking, but I don't understand what prevents the kernel to type-check it without the id
in this case? Or is it a limitation of the elaborator?
constant F : ℕ → Prop
axiom h₁ : F 1
axiom h₂ : ∀ (P : Prop), F 0 → P
axiom h₃ : ∀ (P : ℕ → Prop) (n : ℕ), F n → P 1 → P n
def f : ℕ → ℕ
| (n + 2) := 0
| _ := 1
example {P : Prop} {n : ℕ} (h : F (n + 2)) : P :=
h₂ P (h₃ (λ x, F (f x)) (n + 2) h h₁)
example {P : Prop} {n : ℕ} (h : F (n + 2)) : P :=
h₂ P (id h₃ (λ x, F (f x)) (n + 2) h h₁)
Last updated: Dec 20 2023 at 11:08 UTC