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 ids 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