Lean crashing

Stream: general

[Koundinya Vajjha]

universe u

open nat

variable {α : Type u}
def vec : Type u → ℕ → Type*
| A 0 := punit
| A (succ k) := A × vec A k

inductive dfin : ℕ → Type
| fz {n} : dfin (n+1)
| fs {n} : dfin n → dfin (n+1)

def kth_projn : Π n, vec α n → dfin n → α
| (_) x dfin.fz := x.fst -- crashes lean
| (succ n) (x,xs) (dfin.fs k) := kth_projn n xs k

The above piece of code crashes Lean for me...

[Bryan Gin-ge Chen]

This might also be something fixed in 3.5.0c. I get these errors instead:

14:0: error:
equation compiler failed (use 'set_option trace.eqn_compiler.elim_match true' for additional details)
nested exception message:
cases tactic failed, it is not applicable to the given hypothesis
14:4: error:
equation compiler failed (use 'set_option trace.eqn_compiler.elim_match true' for additional details)
nested exception message:
cases tactic failed, it is not applicable to the given hypothesis

web editor

[Bryan Gin-ge Chen]

Oh wait, nevermind. Somehow it works in the web editor but crashes lean 3.5.0 in vscode...

Edit: I opened an issue for this.