Commit bba7474e authored by Robbert Krebbers's avatar Robbert Krebbers

Add type annotation.

parent 49b5dd50
......@@ -34,7 +34,7 @@ Section definitions.
Context `{pG : proph_mapG P V Σ}.
(** The first resolve for [p] in [pvs] *)
Definition first_resolve (pvs : proph_val_list P V) (p : P) :=
Definition first_resolve (pvs : proph_val_list P V) (p : P) : option V :=
(map_of_list pvs : gmap P V) !! p.
Definition first_resolve_in_list (R : proph_map P V) (pvs : proph_val_list P V) :=
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment