diff options
Diffstat (limited to 'src/Term/Pretty.idr')
| -rw-r--r-- | src/Term/Pretty.idr | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/Term/Pretty.idr b/src/Term/Pretty.idr index ffa88bd..907a073 100644 --- a/src/Term/Pretty.idr +++ b/src/Term/Pretty.idr @@ -120,7 +120,7 @@ getSpline (App (MakePair (t `Over` thin) u _)) = getSpline t = MkSpline (t `Over` Id) [<] getSucs : FullTerm ty ctx -> (Nat, Maybe (FullTerm ty ctx)) -getSucs Zero = (0, Nothing) +getSucs (Lit n) = (n, Nothing) getSucs (Suc t) = mapFst S (getSucs t) getSucs t = (0, Just t) @@ -165,7 +165,7 @@ parameters (names : Stream String) prettyBinding d (assert_smaller t $ getBinding t $ isBoundRefl t) thin prettyFullTerm d t@(App _) thin = prettySpline d (assert_smaller t $ wkn (getSpline t) thin) - prettyFullTerm d Zero thin = lit 0 + prettyFullTerm d (Lit n) thin = lit n prettyFullTerm d (Suc t) thin = let (n, t') = getSucs t in case t' of |