From cedc6109895a53ce6ed667e0391b232bf5463387 Mon Sep 17 00:00:00 2001 From: Chloe Brown Date: Thu, 15 Jun 2023 16:09:42 +0100 Subject: WIP : use smarter weakenings. --- src/Total/Pretty.idr | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'src/Total/Pretty.idr') diff --git a/src/Total/Pretty.idr b/src/Total/Pretty.idr index eade721..aa467d0 100644 --- a/src/Total/Pretty.idr +++ b/src/Total/Pretty.idr @@ -47,7 +47,7 @@ appPrec = App parameters (names : Stream String) export prettyTerm : Len ctx -> Prec -> Term ctx ty -> Doc Syntax - prettyTerm len d (Var i) = bound (pretty $ index (minus (cast len) (S $ elemToNat i)) names) + prettyTerm len d (Var i) = bound (pretty $ index (minus (lenToNat len) (S $ elemToNat i)) names) prettyTerm len d (Abs t) = let Evidence _ (len, t') = getLamNames (S len) t in parenthesise (d > startPrec) $ group $ align $ hang 2 $ @@ -73,7 +73,7 @@ parameters (names : Stream String) bound (pretty $ index offset names) <+> comma <++> prettyBindings' (S offset) (S k) prettyBindings : Len ctx' -> Doc Syntax - prettyBindings k = prettyBindings' (cast len) (minus (cast k) (cast len)) + prettyBindings k = prettyBindings' (lenToNat len) (minus (lenToNat k) (lenToNat len)) prettyTerm len d app@(App t u) = let (f, ts) = getSpline t [prettyArg u] in parenthesise (d >= appPrec) $ group $ align $ hang 2 $ -- cgit v1.2.3