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