From 74f0dc953839179aae071dda1ddb924295bc6061 Mon Sep 17 00:00:00 2001
From: Greg Brown <greg.brown01@ed.ac.uk>
Date: Mon, 2 Jan 2023 15:43:24 +0000
Subject: Add more program structure to type universes.

---
 src/Obs/Term.idr | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

(limited to 'src/Obs/Term.idr')

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 $
-- 
cgit v1.2.3