1@top Program { expression }
2
3expression {
4  expressionPart+
5}
6
7DefinitionBlock {
8  "definition" expression "end"
9}
10
11Proof {
12  "proof" expression "end"
13}
14
15NowBlock {
16  "now" expression "end"
17}
18
19HerebyBlock {
20  "hereby" expression "end"
21}
22
23expressionPart {
24  KeywordControl |
25  SupportFunction |
26  KeywordOther |
27  EntityNameType |
28  ReasoningPhrase |
29  Comment |
30  OpenParen expression CloseParen |
31  OpenBrace expression CloseBrace |
32  OpenBracket expression CloseBracket |
33  DefinitionBlock |
34  Proof |
35  NowBlock |
36  HerebyBlock
37}
38
39@tokens {
40  KeywordControl {
41    "implies" |
42    "holds" |
43    "being" |
44    "for" |
45    "st" |
46    "ex " |
47    "not" |
48    "&" |
49    "or" |
50    "iff"
51  }
52  SupportFunction {
53    "equalities" |
54    "expansions" |
55    "theorem" |
56    "theorems" |
57    "scheme" |
58    "definitions" |
59    "clusters" |
60    "signature" |
61    "vocabulary" |
62    "vocabularies" |
63    "notation" |
64    "notations" |
65    "constructors" |
66    "registration " |
67    "registrations" |
68    "requirements" |
69    "schemes"
70  }
71  KeywordOther {
72    "irreflexivity" |
73    "connectedness" |
74    "compatibility" |
75    "contradiction" |
76    "correctness" |
77    "associativity" |
78    "commutativity" |
79    "consider" |
80    "consistency" |
81    "antonym" |
82    "canceled" |
83    "otherwise" |
84    "reconsider" |
85    "redefine" |
86    "reflexivity" |
87    "symmetry" |
88    "uniqueness" |
89    "transitivity" |
90    "idempotence" |
91    "asymmetry" |
92    "projectivity" |
93    "involutiveness" |
94    "assume" |
95    "cases" |
96    "given" |
97    "per" |
98    "thus" |
99    "take" |
100    "hence" |
101    "is " |
102    "let" |
103    "and" |
104    "attr" |
105    "as" |
106    "be " |
107    "begin" |
108    "cluster" |
109    "coherence" |
110    "def" |
111    "deffunc" |
112    "defpred" |
113    "environ" |
114    "equals" |
115    "existence" |
116    "func" |
117    "if " |
118    "it" |
119    "means" |
120    "mode" |
121    "of" |
122    "over" |
123    "pred" |
124    "provided" |
125    "qua" |
126    "reserve" |
127    "struct" |
128    "such" |
129    "synonym" |
130    "that" |
131    "then" |
132    "thesis" |
133    "where"
134  }
135  EntityNameType {
136    // "proof"，"end"，"now"，"hereby" は削除
137    "case" |
138    "suppose"
139  }
140  Comment { "::" ![\n]* }
141  ReasoningPhrase { ("by" | "from") ![^\n;]* }
142
143  OpenParen { "(" }
144  CloseParen { ")" }
145  OpenBrace { "{" }
146  CloseBrace { "}" }
147  OpenBracket { "[" }
148  CloseBracket { "]" }
149
150  @precedence {
151    Comment,
152    ReasoningPhrase,
153    KeywordControl,
154    SupportFunction,
155    KeywordOther,
156    EntityNameType,
157    OpenParen,
158    CloseParen,
159    OpenBrace,
160    CloseBrace,
161    OpenBracket,
162    CloseBracket
163  }
164}
165
166@external propSource highlighting from "./highlight.js"