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/Syntax.idr | |
| parent | 7e184c20d545afb55f6e962b8bfea882b23699fa (diff) | |
Add more program structure to type universes.
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 $ |