Why is simp! needed in simp_alive_meta #349
Comments
github-merge-queue bot
pushed a commit
that referenced
this issue
May 28, 2024
- add `ConcreteOrMVar.instantiate_ofNat_eq` to simplify instantiation and canonicalize to ofNat. Unfortunately, this seems to lead to a 'motive not type correct' error. To resolve it we use simp! that just unfolds. This should be debugged further: #349. - generalize `toSnoc_toMap` to work on sequences of snoc --------- Co-authored-by: Siddharth <[email protected]>
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Lean is complaining about
motive not type correct. @bollu and I debugged for an hour and could not figure out what's wrong.The text was updated successfully, but these errors were encountered: