diff options
Diffstat (limited to 'src/gen_lib/prompt_monad.lem')
| -rw-r--r-- | src/gen_lib/prompt_monad.lem | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/src/gen_lib/prompt_monad.lem b/src/gen_lib/prompt_monad.lem index 9eb59319..87c9af39 100644 --- a/src/gen_lib/prompt_monad.lem +++ b/src/gen_lib/prompt_monad.lem @@ -212,3 +212,10 @@ let barrier bk = Barrier bk (Done ()) val footprint : forall 'rv 'e. unit -> monad 'rv unit 'e let footprint _ = Footprint (Done ()) + +(* Define a type synonym that also takes the register state as a type parameter, + in order to make switching to the state monad without changing generated + definitions easier, see also lib/hol/prompt_monad.lem. *) + +type base_monad 'regval 'regstate 'a 'e = monad 'regval 'a 'e +type base_monadR 'regval 'regstate 'a 'r 'e = monadR 'regval 'a 'r 'e |