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
inductiveOdd : Nat → Prop
| one : Odd 1
| add_two : Odd n → Odd (n + 2)
theoremodd_iff {n : Nat} : Odd n ↔ n % 2 = 1 := by
refine ⟨fun h => by induction h <;> omega, ?_⟩
match n with
| 0 => simp
| 1 => exact fun _ => Odd.one
| n + 2 => exact fun _ => Odd.add_two (odd_iff.mpr (by omega))
example {n : Nat} : n % 2 = 1 → Odd n := by exact?
the suggestion we get from exact? is Try this: exact fun a => (fun {n} => odd_iff.mpr) a, but this does not work. Accepting the suggestion leads to the two errors
failed to infer binder type
and
don't know how to synthesize implicit argument 'n'
(@fun {n_1} => odd_iff.mpr) (?m.2120 a) a
context:
n : Nat
a : n % 2 = 1
⊢ ?m.2119 a
Expected behavior:exact? suggests some invocation of odd_iff that works
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
In this code:
the suggestion we get from
exact?
isTry this: exact fun a => (fun {n} => odd_iff.mpr) a
, but this does not work. Accepting the suggestion leads to the two errorsand
Expected behavior:
exact?
suggests some invocation ofodd_iff
that worksActual behavior: Suggestion leads to error above
Versions
4.12.0-nightly-2024-09-19
on live.lean-lang.orgImpact
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: