summaryrefslogtreecommitdiff
path: root/src/gen_lib/prompt.lem
diff options
context:
space:
mode:
authorBrian Campbell2018-02-27 11:10:04 +0000
committerBrian Campbell2018-02-27 11:22:20 +0000
commitcb87073e8049f9bbad8da91bdd14c8554e9f846d (patch)
tree1c80d151a5bf88e03b1dfe58dd7d808943b156f9 /src/gen_lib/prompt.lem
parenta8d905a0628c783b564e1ac35de3c93e9dad2956 (diff)
Lem/OCaml compatibility fixes
Diffstat (limited to 'src/gen_lib/prompt.lem')
-rw-r--r--src/gen_lib/prompt.lem7
1 files changed, 5 insertions, 2 deletions
diff --git a/src/gen_lib/prompt.lem b/src/gen_lib/prompt.lem
index bca09aa1..9642c714 100644
--- a/src/gen_lib/prompt.lem
+++ b/src/gen_lib/prompt.lem
@@ -20,10 +20,13 @@ let iter f xs = iteri (fun _ x -> f x) xs
val foreachM : forall 'a 'rv 'vars 'e.
list 'a -> 'vars -> ('a -> 'vars -> monad 'rv 'vars 'e) -> monad 'rv 'vars 'e
-let rec foreachM [] vars _ = return vars
-and foreachM (x :: xs) vars body =
+let rec foreachM l vars body =
+match l with
+| [] -> return vars
+| (x :: xs) ->
body x vars >>= fun vars ->
foreachM xs vars body
+end
declare {isabelle} termination_argument foreachM = automatic