aboutsummaryrefslogtreecommitdiff
path: root/discocaml/eval.ml
diff options
context:
space:
mode:
Diffstat (limited to 'discocaml/eval.ml')
-rw-r--r--discocaml/eval.ml9
1 files changed, 3 insertions, 6 deletions
diff --git a/discocaml/eval.ml b/discocaml/eval.ml
index 63dd6f7..816d269 100644
--- a/discocaml/eval.ml
+++ b/discocaml/eval.ml
@@ -1,8 +1,5 @@
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
-let reduce : expr -> path -> expr = fun e _ -> e
+let find_redex_cbv : expr ast -> expr index option = function _ -> None
+let find_redex_cbn : expr ast -> expr index option = function _ -> None
+let reduce : expr ast -> expr index -> expr ast = fun e _ -> e