Zulip Chat Archive

Stream: general

Topic: assertion violation

Kevin Buzzard (Mar 26 2018 at 20:35):

Kenny found an assertion violation back in Feb or so: instance foo (α : Type) : group α := { mul_assoc := λ x y z, rfl }. I just mention it here because it still seems to be there.

Kevin Buzzard (Mar 26 2018 at 20:35):

Should I file an issue?

Patrick Massot (May 23 2018 at 19:58):

An old friend is back:

m_ctx.match(e, *val2)
LEAN ASSERTION VIOLATION
File: /home/travis/build/leanprover/lean/src/frontends/lean/elaborator.cpp
Line: 3167

Kevin Buzzard (May 23 2018 at 20:08):

did you catch it?

Kevin Buzzard (May 23 2018 at 20:08):

It's always line 3167

Kevin Buzzard (May 23 2018 at 20:08):

they should fix that line

Kevin Buzzard (May 23 2018 at 20:08):

maybe remove the assertion

Patrick Massot (May 23 2018 at 20:10):

I don't think this qualifies as serious enough for a Lean 3.X fix

Kevin Buzzard (May 23 2018 at 20:10):

Can you reproduce it?

Patrick Massot (May 23 2018 at 20:12):

Right now it happens every time I touch anything in my norms.lean

Last updated: Dec 20 2023 at 11:08 UTC