Zulip Chat Archive

Stream: general

Topic: Lean crashing


Koundinya Vajjha (Jun 07 2019 at 14:36):

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 (Jun 07 2019 at 16:03):

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 (Jun 07 2019 at 16:07):

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.


Last updated: Dec 20 2023 at 11:08 UTC