diff options
Diffstat (limited to 'src/gen_lib/prompt.lem')
| -rw-r--r-- | src/gen_lib/prompt.lem | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/src/gen_lib/prompt.lem b/src/gen_lib/prompt.lem index 8cef266e..8214bf49 100644 --- a/src/gen_lib/prompt.lem +++ b/src/gen_lib/prompt.lem @@ -4,6 +4,14 @@ open import Sail_values open import Prompt_monad open import {isabelle} `Prompt_monad_lemmas` +val (>>=) : forall 'rv 'a 'b 'e. monad 'rv 'a 'e -> ('a -> monad 'rv 'b 'e) -> monad 'rv 'b 'e +declare isabelle target_rep function (>>=) = infix `\<bind>` +let inline ~{isabelle} (>>=) = bind + +val (>>) : forall 'rv 'b 'e. monad 'rv unit 'e -> monad 'rv 'b 'e -> monad 'rv 'b 'e +declare isabelle target_rep function (>>) = infix `\<then>` +let inline ~{isabelle} (>>) m n = m >>= fun (_ : unit) -> n + val iter_aux : forall 'rv 'a 'e. integer -> (integer -> 'a -> monad 'rv unit 'e) -> list 'a -> monad 'rv unit 'e let rec iter_aux i f xs = match xs with | x :: xs -> f i x >> iter_aux (i + 1) f xs |