2
私はMap
とPartialMap
と呼ばれる一対のタイプメスを定義しました。特に、それらは、V
またはoption V
を超えているかどうかでのみ異なります。`PartialMap` typeclassに` Map`型を特化する
PartialMap
は、本質的にはMap
という特殊なケースです。しかし、私はそれをどのようにエンコードするのか分かりません。
Class Map M K V: Type := {
get: M K V -> K -> V;
set: M K V -> K -> V -> M K V;
map_get_set_idem: forall (m: M K V) (k: K) (v: V), get (set m k v) k = v;
map_get_set_comm: forall (m: M K V) (k1 k2: K) (v: V), ~(k1 = k2) -> get (set m k1 v) k2 = get m k2;
}.
Class PartialMap M K V: Type := {
pget: M K V -> K -> option V;
pset: M K V -> K -> option V -> M K V;
pmap_pget_pset_idem: forall (m: M K V) (k: K) (v: option V), pget (pset m k v) k = v;
pmap_pget_pset_comm: forall (m: M K V) (k1 k2: K) (v: option V), ~(k1 = k2) -> pget (pset m k1 v) k2 = pget m k2;
}.