spot the difference

Stream: new members

[Kenny Lau]

invalid type ascription, term has type
  @function.injective.{1 1} (pre_von_Neumann n) (pre_von_Neumann m)
    (@nat.le_rec_on.{1} (λ (n : nat), pre_von_Neumann n) (λ (n : nat), @pre_von_Neumann.next n) n m H)
but is expected to have type
  @function.injective.{1 1} (pre_von_Neumann n) (pre_von_Neumann m)
    (@nat.le_rec_on.{1} pre_von_Neumann (λ (n : nat), @pre_von_Neumann.next n) n m H)

state:
n m : nat,
H : @has_le.le.{0} nat nat.has_le n m
⊢ @function.injective.{1 1} (pre_von_Neumann n) (pre_von_Neumann m)
    (@nat.le_rec_on.{1} pre_von_Neumann (λ (n : nat), @pre_von_Neumann.next n) n m H)

[Johan Commelin]

Ouch... that must hurt. (λ (n : nat), pre_von_Neumann n) ought to be defeq to pre_von_Neumann.

[Kenny Lau]

ok convert [...]; ext; refl worked

[Kenny Lau]

@Sebastian Ullrich will this be fixed in Lean 4?

[Kenny Lau]

MWE:

def A : ℕ → Type
| nat.zero     := empty
| (nat.succ n) := A n → empty

example : A = λ n, A n := rfl -- fails

@Mario Carneiro

[Kevin Buzzard]

"Probably a bug", says Sebastian