aboutsummaryrefslogtreecommitdiff
path: root/discocaml/eval.ml
diff options
context:
space:
mode:
Diffstat (limited to 'discocaml/eval.ml')
-rw-r--r--discocaml/eval.ml7
1 files changed, 7 insertions, 0 deletions
diff --git a/discocaml/eval.ml b/discocaml/eval.ml
new file mode 100644
index 0000000..68bb637
--- /dev/null
+++ b/discocaml/eval.ml
@@ -0,0 +1,7 @@
+open Ast
+
+type path = int list
+(** A path from the root of a term to a subterm. *)
+
+let find_redex_cbv : expr -> path option = function _ -> None
+let find_redex_cbn : expr -> path option = function _ -> None