Skip to content

Instantly share code, notes, and snippets.

@efvincent

efvincent/partial_maps.v

Created November 24, 2022 17:38
Show Gist options

  • Select an option

    Learn more about clone URLs
  • Save efvincent/2dc0cd023dea2700d726fe7a1420a9cc to your computer and use it in GitHub Desktop.

Select an option

Learn more about clone URLs
Save efvincent/2dc0cd023dea2700d726fe7a1420a9cc to your computer and use it in GitHub Desktop.
Download ZIP
Raw
partial_maps.v
Inductive partial_map : Type :=
| Empty
| Binding (k : nat) (v : nat) (m : partial_map).
(** update given in the lecture. map will continue to grow, updated
pairs aren't removed - not a realistic representation is it? *)
Definition update' (k v : nat) (m : partial_map) : partial_map :=
Binding k v m.
(** alternative that replaces the updated node at the key *)
Fixpoint update (k v : nat) (m : partial_map) : partial_map :=
match m with
| Empty => Binding k v Empty
| Binding k' v' m' =>
if k =? k'
then Binding k v m'
else Binding k' v' (update k v m')
end.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment