blob: 9ab45753681b45f774725344a72f2b7cfeb2fef1 (
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
|
incomplete concrete TheoryI of Theory =
open
LexTheory,
Grammar,
Symbolic,
Symbol,
Combinators,
Constructors,
(C=ConstructX),
Prelude
in {
lincat
Chapter = Text ;
Jment = Text ;
Decl = Text ;
Prop = S ;
Branch = S ;
Proof = Text ;
[Proof] = Text ;
Typ = CN ;
Obj = NP ;
Label = NP ;
Adverb = PConj ;
Ref = NP ;
[Ref] = [NP] ;
Number = Num ;
lin
Chap title jments =
appendText (mkText (mkPhr (mkUtt title)) TEmpty) jments ;
JDefObj decl a b =
appendText decl (mkUtt (mkS (pred b a))) ;
DProp p =
mkText (mkPhr (mkUtt (mkImp (mkVP assume_VS p)))) TEmpty ;
DTyp a ty = --- x pro a: refresh bug
mkText (mkPhr (mkUtt (mkImp (mkVP assume_VS (mkS (pred ty a)))))) TEmpty ;
PProp p = mkText (mkPhr p) TEmpty ;
PAdvProp a p = mkText (mkPhr a (mkUtt p) NoVoc) TEmpty ;
PDecl d = d ;
PBranch b ps = mkText (mkPhr b) ps ;
BCases n =
mkS (pred have_V2 (mkNP we_Pron) (mkNP (mkDet (mkNum n2)) case_N)) ;
ARef h = mkAdv by8means_Prep h ;
AHence = therefore_PConj ;
AAFort = C.mkPConj ["a fortiori"] ;
RLabel h = h ;
RMany rs = mkNP and_Conj rs ;
}
|
