@@ -579,33 +579,62 @@ mutual
579579 quote (PVTy x) = `(PVTy {a=TT} ~(assert_total (quote x)))
580580
581581mutual
582− quoteRaw : Raw -> TT
583− quoteRaw (Var n) = `(Var ~(quote n))
584− quoteRaw (RBind n b tm) = `(RBind ~(quote n) ~(assert_total $ quoteRawBinder b) ~(quoteRaw tm))
585− quoteRaw (RApp tm tm') = `(RApp ~(quoteRaw tm) ~(quoteRaw tm'))
586− quoteRaw RType = `(RType)
587− quoteRaw (RUType u) = `(RUType ~(quote u))
588− quoteRaw (RForce tm) = `(RForce ~(quoteRaw tm))
589− quoteRaw (RConstant c) = `(RConstant ~(quote c))
590−
591− quoteRawBinder : Binder Raw -> TT
592− quoteRawBinder (Lam x) = `(Lam {a=Raw} ~(quoteRaw x))
593− quoteRawBinder (Pi x k) = `(Pi {a=Raw} ~(quoteRaw x) ~(quoteRaw k))
594− quoteRawBinder (Let x y) = `(Let {a=Raw} ~(quoteRaw x) ~(quoteRaw y))
595− quoteRawBinder (NLet x y) = `(NLet {a=Raw} ~(quoteRaw x) ~(quoteRaw y))
596− quoteRawBinder (Hole x) = `(Hole {a=Raw} ~(quoteRaw x))
597− quoteRawBinder (GHole x) = `(GHole {a=Raw} ~(quoteRaw x))
598− quoteRawBinder (Guess x y) = `(Guess {a=Raw} ~(quoteRaw x) ~(quoteRaw y))
599− quoteRawBinder (PVar x) = `(PVar {a=Raw} ~(quoteRaw x))
600− quoteRawBinder (PVTy x) = `(PVTy {a=Raw} ~(quoteRaw x))
582+ quoteRawTT : Raw -> TT
583+ quoteRawTT (Var n) = `(Var ~(quote n))
584+ quoteRawTT (RBind n b tm) = `(RBind ~(quote n) ~(assert_total $ quoteRawBinderTT b) ~(quoteRawTT tm))
585+ quoteRawTT (RApp tm tm') = `(RApp ~(quoteRawTT tm) ~(quoteRawTT tm'))
586+ quoteRawTT RType = `(RType)
587+ quoteRawTT (RUType u) = `(RUType ~(quote u))
588+ quoteRawTT (RForce tm) = `(RForce ~(quoteRawTT tm))
589+ quoteRawTT (RConstant c) = `(RConstant ~(quote c))
590+
591+ quoteRawBinderTT : Binder Raw -> TT
592+ quoteRawBinderTT (Lam x) = `(Lam {a=Raw} ~(quoteRawTT x))
593+ quoteRawBinderTT (Pi x k) = `(Pi {a=Raw} ~(quoteRawTT x) ~(quoteRawTT k))
594+ quoteRawBinderTT (Let x y) = `(Let {a=Raw} ~(quoteRawTT x) ~(quoteRawTT y))
595+ quoteRawBinderTT (NLet x y) = `(NLet {a=Raw} ~(quoteRawTT x) ~(quoteRawTT y))
596+ quoteRawBinderTT (Hole x) = `(Hole {a=Raw} ~(quoteRawTT x))
597+ quoteRawBinderTT (GHole x) = `(GHole {a=Raw} ~(quoteRawTT x))
598+ quoteRawBinderTT (Guess x y) = `(Guess {a=Raw} ~(quoteRawTT x) ~(quoteRawTT y))
599+ quoteRawBinderTT (PVar x) = `(PVar {a=Raw} ~(quoteRawTT x))
600+ quoteRawBinderTT (PVTy x) = `(PVTy {a=Raw} ~(quoteRawTT x))
601601
602602instance Quotable Raw TT where
603603 quotedTy = `(Raw)
604− quote = quoteRaw
604+ quote = quoteRawTT
605605
606606instance Quotable (Binder Raw) TT where
607607 quotedTy = `(Binder Raw)
608− quote = quoteRawBinder
608+ quote = quoteRawBinderTT
609+
610+mutual
611+ quoteRawRaw : Raw -> Raw
612+ quoteRawRaw (Var n) = `(Var ~(quote n))
613+ quoteRawRaw (RBind n b tm) = `(RBind ~(quote n) ~(assert_total $ quoteRawBinderRaw b) ~(quoteRawRaw tm))
614+ quoteRawRaw (RApp tm tm') = `(RApp ~(quoteRawRaw tm) ~(quoteRawRaw tm'))
615+ quoteRawRaw RType = `(RType)
616+ quoteRawRaw (RUType u) = `(RUType ~(quote u))
617+ quoteRawRaw (RForce tm) = `(RForce ~(quoteRawRaw tm))
618+ quoteRawRaw (RConstant c) = `(RConstant ~(quote c))
619+
620+ quoteRawBinderRaw : Binder Raw -> Raw
621+ quoteRawBinderRaw (Lam x) = `(Lam {a=Raw} ~(quoteRawRaw x))
622+ quoteRawBinderRaw (Pi x k) = `(Pi {a=Raw} ~(quoteRawRaw x) ~(quoteRawRaw k))
623+ quoteRawBinderRaw (Let x y) = `(Let {a=Raw} ~(quoteRawRaw x) ~(quoteRawRaw y))
624+ quoteRawBinderRaw (NLet x y) = `(NLet {a=Raw} ~(quoteRawRaw x) ~(quoteRawRaw y))
625+ quoteRawBinderRaw (Hole x) = `(Hole {a=Raw} ~(quoteRawRaw x))
626+ quoteRawBinderRaw (GHole x) = `(GHole {a=Raw} ~(quoteRawRaw x))
627+ quoteRawBinderRaw (Guess x y) = `(Guess {a=Raw} ~(quoteRawRaw x) ~(quoteRawRaw y))
628+ quoteRawBinderRaw (PVar x) = `(PVar {a=Raw} ~(quoteRawRaw x))
629+ quoteRawBinderRaw (PVTy x) = `(PVTy {a=Raw} ~(quoteRawRaw x))
630+
631+instance Quotable Raw Raw where
632+ quotedTy = `(Raw)
633+ quote = quoteRawRaw
634+
635+instance Quotable (Binder Raw) Raw where
636+ quotedTy = `(Binder Raw)
637+ quote = quoteRawBinderRaw
609638
610639instance Quotable ErrorReportPart TT where
611640 quotedTy = `(ErrorReportPart)