diff options
| author | Malte Voos <git@mal.tc> | 2024-02-20 12:48:36 +0100 |
|---|---|---|
| committer | Malte Voos <git@mal.tc> | 2024-02-20 12:48:36 +0100 |
| commit | 5252fe93e5e7ef77888c06c97de4e350dce90448 (patch) | |
| tree | da057c49ece07e6fd80ec55ad59fbf337162063a /lib/Eval.ml | |
| parent | 407a2a4a0a440c41adc19fbe8b67283b7b7c65ab (diff) | |
| download | toytt-5252fe93e5e7ef77888c06c97de4e350dce90448.tar.gz toytt-5252fe93e5e7ef77888c06c97de4e350dce90448.zip | |
nbe: quotation
Diffstat (limited to 'lib/Eval.ml')
| -rw-r--r-- | lib/Eval.ml | 3 |
1 files changed, 2 insertions, 1 deletions
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 |