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