Skip to content
Snippets Groups Projects
Verified Commit 38df0d21 authored by Paolo G. Giarrusso's avatar Paolo G. Giarrusso
Browse files

Rename Awesome_{ne,proper} to NamespaceMap_{ne,proper}

parent 62798412
No related branches found
No related tags found
No related merge requests found
......@@ -46,9 +46,9 @@ Instance namespace_map_dist : Dist (namespace_map A) := λ n x y,
namespace_map_data_proj x {n} namespace_map_data_proj y
namespace_map_token_proj x = namespace_map_token_proj y.
Global Instance Awesome_ne : NonExpansive2 (@NamespaceMap A).
Global Instance NamespaceMap_ne : NonExpansive2 (@NamespaceMap A).
Proof. by split. Qed.
Global Instance Awesome_proper : Proper (() ==> (=) ==> ()) (@NamespaceMap A).
Global Instance NamespaceMap_proper : Proper (() ==> (=) ==> ()) (@NamespaceMap A).
Proof. by split. Qed.
Global Instance namespace_map_data_proj_ne: NonExpansive (@namespace_map_data_proj A).
Proof. by destruct 1. Qed.
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment