Zulip Chat Archive

Stream: lean4

Topic: simp failing with "application type mismatch Eq.ndrec ..."

David Renshaw (Dec 10 2021 at 19:45):

I have some code the broke between nightly-2021-11-24 and nightly-2021-11-25.
A simp that used to work started failing with "application type mismatch".
See https://github.com/dwrensha/lean4-maze/issues/1.

David Renshaw (Dec 10 2021 at 19:47):

It feels wrong to me that simp could cause a "type mismatch".

David Renshaw (Dec 10 2021 at 19:47):

Does anyone have any hints on how I could debug this?

Leonardo de Moura (Dec 10 2021 at 20:01):

Could you please create a self contained example that exposes the issue?

David Renshaw (Dec 10 2021 at 20:10):

Added a self-contained example here: https://github.com/dwrensha/lean4-maze/issues/1#issuecomment-991262170

Leonardo de Moura (Dec 16 2021 at 01:11):

@David Renshaw I pushed a fix for this bug.

Leonardo de Moura (Dec 16 2021 at 01:14):

BTW, could you please add the tag lean4 to your repo? Then, others can find it here:
https://github.com/topics/lean4

David Renshaw (Dec 16 2021 at 01:45):

added "lean4" as a topic for the repo

Last updated: Dec 20 2023 at 11:08 UTC