Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion src/Lean/Meta/Tactic/Grind/EMatchTheorem.lean
Original file line number Diff line number Diff line change
Expand Up @@ -716,7 +716,7 @@ where
pure dontCare
else
let arg ← expandOffsetPatterns arg
unless isEqBwdParent do
unless isEqBwdParent || inSupport do
/-
**Note**: We ignore symbols in ground patterns if the parent is the auxiliary ``Grind.eqBwdPattern
We do that because we want to sign an error in examples such as:
Expand Down
43 changes: 43 additions & 0 deletions tests/lean/run/grind_ground_pat_issue.lean
Original file line number Diff line number Diff line change
@@ -0,0 +1,43 @@
/-!
Test for a regression introduced by #11589
-/

section Mathlib.Order.Defs.LinearOrder

class LinearOrder (α : Type) extends Max α where

end Mathlib.Order.Defs.LinearOrder
section Mathlib.Data.Int.Order.Basic

instance instLinearOrder : LinearOrder Int where

end Mathlib.Data.Int.Order.Basic
section Mathlib.Order.Lattice

variable {α : Type}

class SemilatticeSup (α : Type) where
sup : α → α → α

instance SemilatticeSup.toMax [SemilatticeSup α] : Max α where max a b := SemilatticeSup.sup a b

instance LinearOrder.toSemilatticeSup {α : Type} [LinearOrder α] : SemilatticeSup α where
sup := max

end Mathlib.Order.Lattice

section Mathlib.Algebra.Order.Group.Unbundled.Abs

variable {α : Type} [SemilatticeSup α] [Neg α] {a b : α}

@[grind]
def abs (a : α) : α := max a (-a)

end Mathlib.Algebra.Order.Group.Unbundled.Abs

@[grind =] theorem max_def [Max α] [LE α] [DecidableLE α] (a b : α)
: max a b = if a ≤ b then b else a :=
sorry

theorem abs_lt_one_iff {a : Int} : abs a < 1 ↔ a = 0 := by
grind
Loading