max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: missing Option lemma (#9028)

Browse source
This commit is contained in:
Kim Morrison 2025-06-27 17:28:59 +10:00 • committed by GitHub
parent 0aca10b228
commit 8d40cf5157
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 4 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/Init/Data/Option/Lemmas.lean
View file

@ -645,6 +645,10 @@ theorem get_none_eq_iff_true {h} : (none : Option α).get h = a ↔ True := by
simp only [guard]
split <;> simp
@[grind =] theorem getD_guard : (guard p a).getD b = if p a then a else b := by
simp only [guard]
split <;> simp
@[grind]
theorem guard_def (p : α → Bool) :
Option.guard p = fun x => if p x then some x else none := rfl