implement typechecking

1 files changed, 7 insertions, 7 deletions

diff --git a/lib/Quote.ml b/lib/Quote.ml
index 5989870..611843a 100644
--- a/lib/Quote.ml
+++ b/lib/Quote.ml
@@ -15,28 +15,28 @@ struct
     
   let rec quote = function
     | D.Neutral ne -> quote_ne ne
-    | D.Pi (base, fam) -> S.Pi (quote base, quote_clos fam)
-    | D.Lam clos -> S.Lam (quote_clos clos)
-    | D.Sg (base, fam) -> S.Sg (quote base, quote_clos fam)
+    | D.Pi (base, fam) -> S.Pi (quote base, quote_clo fam)
+    | D.Lam clo -> S.Lam (quote_clo clo)
+    | D.Sg (base, fam) -> S.Sg (quote base, quote_clo fam)
     | D.Pair (v, w) -> S.Pair (quote v, quote w)
     | D.Type -> S.Type
     | D.Bool -> S.Bool
     | D.True -> S.True
     | D.False -> S.False
 
-  and quote_clos clos = bind @@ fun arg -> quote (Eval.inst_clos clos arg)
+  and quote_clo clo = bind @@ fun arg -> quote (Eval.inst_clo clo arg)
 
-  and quote_ne (hd, frms) = Bwd.fold_left quote_frame (quote_ne_head hd) frms
+  and quote_ne (hd, frms) = Bwd.fold_left quote_frm (quote_ne_head hd) frms
 
   and quote_ne_head (D.Var i) = S.Var (Eff.read() - i - 1) (* converting from levels to indices *)
 
-  and quote_frame hd = function
+  and quote_frm hd = function
     | D.App v -> S.App (hd, quote v)
     | D.Fst -> S.Fst hd
     | D.Snd -> S.Snd hd
     | D.BoolElim { cmot; vtrue; vfalse } ->
       S.BoolElim {
-        motive = quote_clos cmot;
+        motive = quote_clo cmot;
         true_case = quote vtrue;
         false_case = quote vfalse;
         scrut = hd;