blob: 16eaa96c9218c379d03896def400669bb693d813 (
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
|
module Obs.Sort
-- 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) = True
_ == _ = False
export
Show Sort where
show Prop = "Prop"
show (Set 0) = "Set"
show (Set (S i)) = "Set \{show (S i)}"
-- Operations ------------------------------------------------------------------
infix 5 ~>
public export
suc : Sort -> Sort
suc Prop = Set 0
suc (Set i) = Set (S 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)
|
