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
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
|
interface Prooftext = open
Grammar,
LexTheory,
Symbolic,
Symbol,
(C=ConstructX),
Constructors,
Combinators
in {
oper
Chapter = Text ;
Section = Text ;
Sections = Text ;
Decl = Text ;
Decls = Text ;
Prop = S ;
Branching= S ;
Proof = Text ;
Proofs = Text ;
Typ = CN ;
Object = NP ;
Label = NP ;
Adverb = PConj ;
Ref = NP ;
Refs = [NP] ;
Number = Num ;
chapter : Label -> Sections -> Chapter
= \title,jments ->
appendText (mkText (mkPhr (mkUtt title)) TEmpty) jments ;
definition : Decls -> Object -> Object -> Section
= \decl,a,b ->
appendText decl (mkText (mkPhr (mkUtt (mkS (pred b a)))) TEmpty) ;
theorem : Prop -> Proof -> Section
= \prop,prf -> appendText (mkText (mkPhr prop) TEmpty) prf ;
assumption : Prop -> Decl
= \p ->
mkText (mkPhr (mkUtt (mkImp (mkVP assume_VS p)))) TEmpty ;
declaration : Object -> Typ -> Decl
= \a,ty ->
mkText (mkPhr (mkUtt (mkImp (mkVP assume_VS (mkS (pred ty a)))))) TEmpty ;
proof = overload {
proof : Prop -> Proof
= \p -> mkText (mkPhr p) TEmpty ;
proof : Str -> Proof
= \s -> {s = s ++ "." ; lock_Text = <>} ;
proof : Adverb -> Prop -> Proof
= \a,p -> mkText (mkPhr a (mkUtt p) NoVoc) TEmpty ;
proof : Decl -> Proof
= \d -> d ;
proof : Proof -> Proof -> Proof
= appendText ;
proof : Branching -> Proofs -> Proof
= \b,ps -> mkText (mkPhr b) ps
} ;
proofs : Proof -> Proof -> Proofs
= appendText ;
cases : Num -> Branching
= \n ->
mkS (pred have_V2 (mkNP we_Pron) (mkNP (mkDet n) case_N)) ;
by : Ref -> Adverb
= \h -> C.mkPConj (mkAdv by8means_Prep h).s ;
therefore : Adverb
= therefore_PConj ;
afortiori : Adverb
= C.mkPConj ["a fortiori"] ;
hypothesis : Adverb
= C.mkPConj (mkAdv by8means_Prep (mkNP (mkDet DefArt) hypothesis_N)).s ;
ref : Label -> Ref
= \h -> h ;
refs : Refs -> Ref
= \rs -> mkNP and_Conj rs ;
mkLabel : Str -> Label ;
}
|
