blob: bbd69753cb1e653e8bbc8ac7cb32cb0b3b04aa74 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
|
module Obs.Sort
import Text.PrettyPrint.Prettyprinter
%default total
-- Definition ------------------------------------------------------------------
public export
data Sort : Type where
Prop : Sort
Set : Nat -> Sort
%name Sort s, s', s'', s'''
-- Interfaces ------------------------------------------------------------------
export
Eq Sort where
Prop == Prop = True
(Set i) == (Set j) = i == j
_ == _ = False
export
Show Sort where
show Prop = "Prop"
show (Set 0) = "Set"
show (Set (S i)) = "Set \{show (S i)}"
export
Pretty Sort where
prettyPrec d Prop = pretty "Prop"
prettyPrec d (Set 0) = pretty "Set"
prettyPrec d (Set (S i)) = parenthesise (d >= App) $ pretty "Set \{show (S i)}"
-- Operations ------------------------------------------------------------------
infix 5 ~>
public export
suc : Sort -> Sort
suc Prop = Set 0
suc (Set i) = Set (S i)
public export
ensureSet : Sort -> Sort
ensureSet Prop = Set 0
ensureSet (Set i) = Set i
public export
lub : Sort -> Sort -> Sort
lub Prop s' = s'
lub (Set i) Prop = Set i
lub (Set i) (Set j) = Set (max i j)
public export
(~>) : Sort -> Sort -> Sort
s ~> Prop = Prop
s ~> (Set k) = lub s (Set k)
|
