Skip to content

Commit

Permalink
fix: simp fails to discharge autoParam premises even when it can …
Browse files Browse the repository at this point in the history
…reduce them to `True` (leanprover#3314)

closes leanprover#3257
  • Loading branch information
leodemoura authored and arthur-adjedj committed Feb 19, 2024
1 parent 435fe6a commit 2bc44f6
Show file tree
Hide file tree
Showing 2 changed files with 19 additions and 0 deletions.
1 change: 1 addition & 0 deletions src/Lean/Meta/Tactic/Simp/Rewrite.lean
Original file line number Diff line number Diff line change
Expand Up @@ -471,6 +471,7 @@ where
return some mvarId

def dischargeDefault? (e : Expr) : SimpM (Option Expr) := do
let e := e.cleanupAnnotations
if isEqnThmHypothesis e then
if let some r ← dischargeUsingAssumption? e then
return some r
Expand Down
18 changes: 18 additions & 0 deletions tests/lean/run/3257.lean
Original file line number Diff line number Diff line change
@@ -0,0 +1,18 @@
structure T : Prop
structure U : Prop

theorem foo : T → U := λ _ => {}
theorem bar : (_ : T := by trivial) → U := λ _ => {}

-- fails as expected
example : U := by
fail_if_success simp
sorry

-- works as expected, discharging `T` via `T.mk`
example : U := by
simp [foo, T.mk]

example : U := by
set_option trace.Meta.Tactic.simp true in
simp [bar, T.mk]

0 comments on commit 2bc44f6

Please sign in to comment.