diff options
| author | Chloe Brown <chloe.brown.00@outlook.com> | 2023-07-03 18:21:50 +0100 |
|---|---|---|
| committer | Chloe Brown <chloe.brown.00@outlook.com> | 2023-07-03 18:21:50 +0100 |
| commit | 9039055d9a994bde34e0c0bfedad1a72cd9c17a7 (patch) | |
| tree | d9a843875ee25b64797e56889a8788b7910afde5 /src/Term/Pretty.idr | |
| parent | 6385ecf96cd60885c221e3144b5a5ec63eb5c831 (diff) | |
Add literals as primitive term.
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 |