diff options
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 $ |