Skip to content

Commit

Permalink
remove unused variable
Browse files Browse the repository at this point in the history
  • Loading branch information
datokrat committed Jan 13, 2025
1 parent 1f95486 commit c78646b
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion src/Std/Data/DHashMap/Internal/List/Associative.lean
Original file line number Diff line number Diff line change
Expand Up @@ -2022,7 +2022,7 @@ theorem length_alterKey [BEq α] [EquivBEq α] {k : α} {f : Option β → Optio
containsKey_eq_isSome_getValue?, ← getValue?_eq_some_getValue, -getValue?_eq_none]

theorem alterKey_cons_perm [BEq α] [EquivBEq α] {k : α} {f : Option β → Option β}
{k' : α} {v' : β} {l : List ((a : α) × β)} :
{k' : α} {v' : β} {l : List ((_ : α) × β)} :
Perm (alterKey k f (⟨k', v'⟩ :: l)) (if k' == k then
match f (some v') with
| none => l
Expand Down

0 comments on commit c78646b

Please sign in to comment.