Skip to content

Commit

Permalink
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
even better Inhabited instance
Browse files Browse the repository at this point in the history
datokrat committed Jan 13, 2025
1 parent 0fff730 commit e1ae125
Showing 1 changed file with 2 additions and 2 deletions.
4 changes: 2 additions & 2 deletions src/Std/Data/DHashMap/Lemmas.lean
Original file line number Diff line number Diff line change
@@ -1073,7 +1073,7 @@ theorem get_alter_self [LawfulBEq α] {k : α} {f : Option (β k) → Option (β
theorem get!_alter [LawfulBEq α] {k k' : α} [hi : Inhabited (β k')] {f : Option (β k) → Option (β k)} :
(m.alter k f).get! k' =
if heq : k == k' then
haveI : Inhabited (β k) := cast (by rw [eq_of_beq heq]) hi
haveI : Inhabited (β k) := cast (congrArg β <| eq_of_beq heq).symm default⟩
cast (congrArg β (eq_of_beq heq)) <| (f (m.get? k)).get!
else
m.get! k' :=
@@ -1402,7 +1402,7 @@ theorem get_modify_self [LawfulBEq α] {k : α} {f : β k → β k} {h : k ∈ m
theorem get!_modify [LawfulBEq α] {k k' : α} [hi : Inhabited (β k')] {f : β k → β k} :
(m.modify k f).get! k' =
if heq : k == k' then
haveI : Inhabited (β k) := cast (by rw [eq_of_beq heq]) hi
haveI : Inhabited (β k) := cast (congrArg β <| eq_of_beq heq).symm default⟩
-- not correct if f does not preserve default: ... f (m.get! k)
-- possible alternative: write ... (m.getD k (cast ⋯ default))
m.get? k |>.map f |>.map (cast (congrArg β (eq_of_beq heq))) |>.get!

0 comments on commit e1ae125

Please sign in to comment.