blob: 778e0a8ecea8bf905e491e70f1a98fd395c9ad36 (
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
|
abstract Theory = {
cat
Chapter ;
Jment ;
[Jment] {0} ;
Decl ;
[Decl] {0} ;
Prop ;
Proof ;
[Proof] {2} ;
Branch ;
Typ ;
Obj ;
Label ;
Ref ;
[Ref] ;
Adverb ;
Number ;
fun
Chap : Label -> [Jment] -> Chapter ; -- title, text
JDefObj : [Decl] -> Obj -> Obj -> Jment ; -- a = b (G)
JDefObjTyp : [Decl] -> Typ -> Obj -> Obj -> Jment ; -- a = b : A (G)
JDefProp : [Decl] -> Prop -> Prop -> Jment ; -- A = B : Prop (G)
JThm : [Decl] -> Prop -> Proof -> Jment ; -- p : P (G)
DProp : Prop -> Decl ; -- assume P
DPropLabel : Label -> Prop -> Label ; -- assume P (h)
DTyp : Obj -> Typ -> Decl ; -- let x,y be T
PProp : Prop -> Proof ; -- P.
PAdvProp : Adverb -> Prop -> Proof ; -- Hence, P.
PDecl : Decl -> Proof ; -- Assume P.
PBranch : Branch -> [Proof] -> Proof ; -- By cases: P1 P2
BCases : Number -> Branch ; -- We have n cases.
ARef : Ref -> Adverb ; -- by Thm 2
AHence : Adverb ; -- therefore
AAFort : Adverb ; -- a fortiori
RLabel : Label -> Ref ; -- Thm 2
RMany : [Ref] -> Ref ; -- Thm 2 and Lemma 4
}
|
