summaryrefslogtreecommitdiff
path: root/src/search.sig
diff options
context:
space:
mode:
authorGravatar FrigoEU <simon.van.casteren@gmail.com>2019-07-31 15:13:18 +0200
committerGravatar FrigoEU <simon.van.casteren@gmail.com>2019-07-31 15:13:18 +0200
commit80e7bb6165a5ad6517b35f301228f56b58eef39c (patch)
treed9f3b42b6cb74ebacc43d4081e5d91aebbe7a20f /src/search.sig
parent83bab4581d9570e151b23db3b4de016600afa76d (diff)
first iteration of "typeOf" command
Diffstat (limited to 'src/search.sig')
-rw-r--r--src/search.sig5
1 files changed, 5 insertions, 0 deletions
diff --git a/src/search.sig b/src/search.sig
index ac867146..2de85425 100644
--- a/src/search.sig
+++ b/src/search.sig
@@ -59,4 +59,9 @@ signature SEARCH = sig
* ('state11 -> 'state2 -> ('state11 * 'state2, 'abort) result)
-> (('state11 * 'state12) * 'state2, 'abort) result
+ val bindPWithPos :
+ (('state11 * 'state12) * 'state2, 'abort) result
+ * (('state11 * 'state12) -> 'state2 -> ('state11 * 'state2, 'abort) result)
+ -> (('state11 * 'state12) * 'state2, 'abort) result
+
end