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
inductiveTywhere
| star: Ty
notation" ✶ " => Ty.star
abbrev Context : Type := List Ty
inductiveLookup : Context → Ty → Type where
| z : Lookup (t :: Γ) t
inductiveTerm : Context → Ty → Type where
| var : Lookup Γ a → Term Γ a
| lam : Term (✶ :: Γ) ✶ → Term Γ ✶
| ap : Term Γ ✶ → Term Γ ✶ → Term Γ ✶
abbrev plus : Term Γ a → Term Γ a
| .var i => .var i
| .lam n => .lam (plus n)
| .ap (.lam _) m => plus m -- This case takes precedence over the next one.
| .ap l m => (plus l).ap (plus m)
-- I with to be able to prove the following "by definition":example : plus (.ap l m) = (plus l).ap (plus m) := by
unfold plus
--^^ failed to generate equality theorems for `match` expression `plus.match_1`
Expected behavior: The plus definition gets unfolded. IIRC since it's recursive, it should be unfolded only once.
Actual behavior: The last line generates the following error message:
failed to generate equality theorems for `match` expression `plus.match_1`
Γ : Context
a : Ty
motive : Term Γ a → Sort u_1
n : Term ( ✶ :: Γ) ✶
h_1 : (i : Lookup Γ a) → motive (Term.var i)
h_2 : (n : Term ( ✶ :: Γ) ✶ ) → motive (Term.lam n)
h_3 : (a : Term ( ✶ :: Γ) ✶ ) → (m : Term Γ ✶ ) → motive (Term.ap (Term.lam a) m)
h_4 : (l m : Term Γ ✶ ) → motive (Term.ap l m)
⊢ Eq.rec (fun x motive h_1 h_2 h_3 h_4 h => (_ : Term.lam n = x) ▸ h_2 n) (_ : ✶ = a) (Term.lam n) motive h_1 h_2 h_3 h_4
(_ : HEq (Term.lam n) (Term.lam n)) =
h_2 n
Prerequisites
Description
Pasted from Zulip:
Expected behavior: The
plus
definition gets unfolded. IIRC since it's recursive, it should be unfolded only once.Actual behavior: The last line generates the following error message:
Reproduces how often: 100%
Versions
lean-toolchain:
leanprover/lean4:nightly-2023-05-16
OS: macOS Ventura 13.4 22F66 arm64
The text was updated successfully, but these errors were encountered: