From 5252fe93e5e7ef77888c06c97de4e350dce90448 Mon Sep 17 00:00:00 2001 From: Malte Voos Date: Tue, 20 Feb 2024 12:48:36 +0100 Subject: nbe: quotation --- lib/Eval.ml | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) (limited to 'lib/Eval.ml') diff --git a/lib/Eval.ml b/lib/Eval.ml index 29ede14..8f6722b 100644 --- a/lib/Eval.ml +++ b/lib/Eval.ml @@ -36,7 +36,7 @@ struct | _ -> invalid_arg "Eval.bool_elim" and eval = function - | S.Var i -> BwdLabels.nth (Eff.read()) i + | S.Var i -> Bwd.nth (Eff.read()) i | S.Pi (base, fam) -> D.Pi (eval base, make_clos fam) | S.Lam body -> D.Lam (make_clos body) | S.App (a, b) -> app (eval a) (eval b) @@ -53,3 +53,4 @@ struct end let eval ~env tm = Internal.Eff.run ~env (fun () -> Internal.eval tm) +let inst_clos = Internal.inst_clos -- cgit 1.4.1