diff options
Diffstat (limited to 'lib/coq/Sail2_prompt_monad.v')
| -rw-r--r-- | lib/coq/Sail2_prompt_monad.v | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/lib/coq/Sail2_prompt_monad.v b/lib/coq/Sail2_prompt_monad.v index f95e4b6c..b26a2ff3 100644 --- a/lib/coq/Sail2_prompt_monad.v +++ b/lib/coq/Sail2_prompt_monad.v @@ -113,6 +113,8 @@ Definition choose_bool {rv E} descr : monad rv bool E := Choose descr returnm. (*val undefined_bool : forall 'rv 'e. unit -> monad 'rv bool 'e*) Definition undefined_bool {rv e} (_:unit) : monad rv bool e := choose_bool "undefined_bool". +Definition undefined_unit {rv e} (_:unit) : monad rv unit e := returnm tt. + (*val assert_exp : forall rv e. bool -> string -> monad rv unit e*) Definition assert_exp {rv E} (exp :bool) msg : monad rv unit E := if exp then Done tt else Fail msg. |