diff options
| author | Greg Brown <greg.brown01@ed.ac.uk> | 2023-01-02 15:43:24 +0000 |
|---|---|---|
| committer | Greg Brown <greg.brown01@ed.ac.uk> | 2023-01-02 15:43:24 +0000 |
| commit | 74f0dc953839179aae071dda1ddb924295bc6061 (patch) | |
| tree | 6a4b29383502ec1ebbe12d5e46f5658d382859d2 /src/Obs/Term.idr | |
| parent | 7e184c20d545afb55f6e962b8bfea882b23699fa (diff) | |
Add more program structure to type universes.
Diffstat (limited to 'src/Obs/Term.idr')
| -rw-r--r-- | src/Obs/Term.idr | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/src/Obs/Term.idr b/src/Obs/Term.idr index 422af87..c4d9e40 100644 --- a/src/Obs/Term.idr +++ b/src/Obs/Term.idr @@ -2,7 +2,7 @@ module Obs.Term import Data.Fin -import Obs.Sort +import Obs.Universe import Text.Bounded import Text.PrettyPrint.Prettyprinter @@ -13,8 +13,8 @@ import Text.PrettyPrint.Prettyprinter public export data Term : Nat -> Type where Var : String -> Fin n -> Term n - -- Sorts - Sort : Sort -> Term n + -- Universes + Universe : Universe -> Term n -- Dependent Product Pi : WithBounds String -> WithBounds (Term n) -> WithBounds (Term (S n)) -> Term n Lambda : WithBounds String -> WithBounds (Term (S n)) -> Term n @@ -74,7 +74,7 @@ prettyPrec : Prec -> Term n -> Doc ann prettyPrecBounds : Prec -> WithBounds (Term n) -> Doc ann prettyPrec d (Var var _) = pretty var -prettyPrec d (Sort s) = prettyPrec d s +prettyPrec d (Universe s) = prettyPrec d s prettyPrec d (Pi var a b) = parenthesise (d > Open) $ group $ |