Skip to content
Snippets Groups Projects
Commit 5602833e authored by Daniel Nezamabadi's avatar Daniel Nezamabadi
Browse files

Constrain lock_name to be Inhabited

parent d18120d1
No related branches found
No related tags found
No related merge requests found
......@@ -26,6 +26,7 @@ Class lock := Lock {
lockG : gFunctors Type;
(** [name] is used to associate [locked] with [is_lock] *)
lock_name : Type;
#[global] lock_name_inhabited :: Inhabited lock_name;
(** * Predicates *)
(** No namespace [N] parameter because we only expose program specs, which
anyway have the full mask. *)
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment