Closed ahelwer closed 8 months ago
Also fixed bugs:
Made some changes to the grammar to help with #94.
Breaking changes are as follows:
identifier:
unbounded_quantification
intro:
label
identifier_ref
identifier
new
level
statement_level
proof_step_id
Non-breaking changes to grammar include:
parameter:
Arity1OrN
quantifier_bound
set:
expression:
choose
statement:
proof:
theorem
Also fixed bugs:
Made some changes to the grammar to help with #94.
Breaking changes are as follows:
identifier:
field name inunbounded_quantification
rule tointro:
label
rule to useidentifier_ref
for parameters instead ofidentifier
new
rule to rule out invalid syntaxlevel
rule name tostatement_level
to avoid collision withlevel
alias inproof_step_id
ruleNon-breaking changes to grammar include:
parameter:
field toArity1OrN
ruleintro:
label for quantifier variables inquantifier_bound
ruleintro:
,set:
, andexpression:
fields tochoose
rulestatement:
andproof:
fields totheorem
rule