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
fin_cases fails on some intervals over the type Fin (k + 2). For example:
import Mathlib.Tactic
example (k : ℕ) (x : Fin (k + 2)) (hx : x ∈ Finset.Iic 1) : True := by
fin_cases hx
and
import Mathlib.Tactic
example (k : ℕ) (x : Fin (k + 2)) (hx : x ∈ Finset.Icc 0 1) : True := by
fin_cases hx
should each create two cases, (x = ⊥ and x = 1 in the first example, x = 0 and x = 1 in the second). Instead they both return the error "(kernel) declaration has metavariables '_example'". More examples of this can be found in this thread on the Lean Zulip.
The text was updated successfully, but these errors were encountered:
fin_cases
fails on some intervals over the typeFin (k + 2)
. For example:and
should each create two cases, (
x = ⊥
andx = 1
in the first example,x = 0
andx = 1
in the second). Instead they both return the error "(kernel) declaration has metavariables '_example'". More examples of this can be found in this thread on the Lean Zulip.The text was updated successfully, but these errors were encountered: