diff options
Diffstat (limited to 'src/Obs/Syntax.idr')
| -rw-r--r-- | src/Obs/Syntax.idr | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/src/Obs/Syntax.idr b/src/Obs/Syntax.idr index 7bf4b61..32e86c0 100644 --- a/src/Obs/Syntax.idr +++ b/src/Obs/Syntax.idr @@ -1,7 +1,7 @@ ||| Raw syntax for terms. This is before eliminating names. module Obs.Syntax -import Obs.Sort +import Obs.Universe import Text.Bounded import Text.PrettyPrint.Prettyprinter @@ -13,8 +13,8 @@ import Text.PrettyPrint.Prettyprinter public export data Syntax : Type where Var : String -> Syntax - -- Sorts - Sort : Sort -> Syntax + -- Universes + Universe : Universe -> Syntax -- Dependent Products Pi : WithBounds String -> WithBounds Syntax -> WithBounds Syntax -> Syntax Lambda : WithBounds String -> WithBounds Syntax -> Syntax @@ -55,7 +55,7 @@ prettyPrec : Prec -> Syntax -> Doc ann prettyPrecBounds : Prec -> WithBounds Syntax -> 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 $ |