diff options
| author | Chloe Brown <chloe.brown.00@outlook.com> | 2023-06-15 16:09:42 +0100 |
|---|---|---|
| committer | Chloe Brown <chloe.brown.00@outlook.com> | 2023-06-15 16:09:42 +0100 |
| commit | cedc6109895a53ce6ed667e0391b232bf5463387 (patch) | |
| tree | cb600a2b91255586821d94dba5137a8cb746c90e /src/Total/Pretty.idr | |
| parent | f910e142ce7c10f8244ecfa40e41756fb8c8a53f (diff) | |
WIP : use smarter weakenings.better-thinning
Diffstat (limited to 'src/Total/Pretty.idr')
| -rw-r--r-- | src/Total/Pretty.idr | 4 |
1 files changed, 2 insertions, 2 deletions
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 $ |