ccc7157c08
This PR adds `@[expose]` to `Lean.Grind.abstractFn` and `Lean.Grind.simpMatchDiscrsOnly` so that the kernel can unfold them when type-checking `grind`-produced proofs inside `module` blocks. Other similar gadgets (`nestedDecidable`, `PreMatchCond`, `alreadyNorm`) were already exposed; these two were simply missed. Closes https://github.com/leanprover/lean4/issues/13167
6 lines
277 B
Text
6 lines
277 B
Text
module
|
||
|
||
-- https://github.com/leanprover/lean4/issues/13167
|
||
theorem Option.bind_pmap {α β γ} {p : α → Prop} (f : ∀ a, p a → β) (x : Option α) (g : β → Option γ) (H) :
|
||
pmap f x H >>= g = x.pbind fun a h ↦ g (f a (H _ h)) := by
|
||
grind [cases Option, pmap]
|