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
Reduced the issue to a self-contained, reproducible test case.
Description
PANIC at Lean.Meta.whnfEasyCases Lean.Meta.WHNF:305:22: unreachable code has been reached
Steps to Reproduce
variable (R : α → α → Prop)
inductive List.Pairwise : List α → Prop
| nil : Pairwise []
| cons : ∀ {a : α} {l : List α}, (∀ {a} (_ : a' ∈ l), R a a') → Pairwise l → Pairwise (a :: l)
theorem and_assoc : (a ∧ b) ∧ c ↔ a ∧ (b ∧ c) :=
⟨fun ⟨⟨ha, hb⟩, hc⟩ => ⟨ha, hb, hc⟩, fun ⟨ha, hb, hc⟩ => ⟨⟨ha, hb⟩, hc⟩⟩
theorem and_left_comm : a ∧ (b ∧ c) ↔ b ∧ (a ∧ c) := by
rw [← and_assoc, ← and_assoc, @And.comm a b]
exact Iff.rfl
theorem pairwise_append {l₁ l₂ : List α} :
(l₁ ++ l₂).Pairwise R ↔ l₁.Pairwise R ∧ l₂.Pairwise R ∧ ∀ {a} (_ : a ∈ l₁), ∀ {b} (_ : b ∈ l₂), R a b := by
induction l₁ <;> simp [*, and_left_comm]
Expected behavior: [What you expect to happen]
Failure with unsolved goals. (I can restore a proper proof if that is better for a test case.)
Actual behavior: [What actually happens]
PANIC at Lean.Meta.whnfEasyCases Lean.Meta.WHNF:305:22: unreachable code has been reached
Prerequisites
Description
PANIC at Lean.Meta.whnfEasyCases Lean.Meta.WHNF:305:22: unreachable code has been reached
Steps to Reproduce
Expected behavior: [What you expect to happen]
Failure with unsolved goals. (I can restore a proper proof if that is better for a test case.)
Actual behavior: [What actually happens]
PANIC at Lean.Meta.whnfEasyCases Lean.Meta.WHNF:305:22: unreachable code has been reached
Versions
Lean (version 4.0.0-nightly-2022-11-16, commit 98922b8, Release)
Additional Information
This is getting in the way of bumping Std4 (and then mathlib4).
The text was updated successfully, but these errors were encountered: