You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
simp only [Fin.isValue] panics in the presence of expression metadata.
An easy way to construct such metadata is @& borrow notation, but in my non-mwe the metadata presumably came from elsewhere.
Context
Steps to Reproduce
Run example : (@& (1 : Fin 2)) = 1 := by simp only [Fin.isValue]
Prerequisites
Please put an X between the brackets as you perform the following steps:
https://github.com/leanprover/lean4/issues
Avoid dependencies to Mathlib or Batteries.
https://live.lean-lang.org/#project=lean-nightly
(You can also use the settings there to switch to “Lean nightly”)
Description
simp only [Fin.isValue]
panics in the presence of expression metadata.An easy way to construct such metadata is
@&
borrow notation, but in my non-mwe the metadata presumably came from elsewhere.Context
Steps to Reproduce
example : (@& (1 : Fin 2)) = 1 := by simp only [Fin.isValue]
Expected behavior: Succeeds
Actual behavior: Panics
Versions
4.11.0-rc1
Additional Information
Note that panics are not shown in the web editor
Impact
Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.
The text was updated successfully, but these errors were encountered: