From 9039055d9a994bde34e0c0bfedad1a72cd9c17a7 Mon Sep 17 00:00:00 2001 From: Chloe Brown Date: Mon, 3 Jul 2023 18:21:50 +0100 Subject: Add literals as primitive term. --- src/Term/Pretty.idr | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'src/Term/Pretty.idr') 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 -- cgit v1.2.3