lean crash with SIGABRT.

Stream: general

[fonqL]

lean version: 4.10.0
code:

def Vect (n: Nat) (A: Type u) := {l: List A // l.length = n}

def Vect.cons (a: A) (v: Vect n A): Vect (n + 1) A :=
  ⟨a::v.val, by simp [v.property]⟩

instance: GetElem (Vect n A) Nat A (λ _ i => i < n) where
  getElem vec i _ := match vec with | ⟨l, _⟩ => l[i]

theorem Vect.aux
    {as: List A} {xm: List (Vect m A)}
    (h0: xm.length = as.length)
    (ih: i < (List.zipWith cons as xm).length)
    (jh: j < m)
    : ((List.zipWith cons as xm)[i])[j + 1] =
        xm[i]'(by simpa[h0] using ih)[j] := by
        -- Correct syntax requires an extra pair of parentheses:
        -- (xm[i]'(by simpa[h0] using ih))[j]
        -- but `lean` should not crash.
  sorry

Running lean filename.lean with code above will make lean exit with SIGABRT.

[Henrik Böving]

Please open an issue on https://github.com/leanprover/lean4

[fonqL]

lean4#4920

[Shreyas Srinivas]

I guess you mean lean4#4920