Syntax change to scheme proposal

--0000000000005c99020648472b42
Content-Type: text/plain; charset="UTF-8"

Hello,

Right now, the syntax for a scheme looks like:

```
Scheme-Block = "scheme" Scheme-Identifier "{" Scheme-Parameters "}" ":"
  Scheme-Conclusion [ "provided" Scheme-Premise { "and" Scheme-Premise } ]
*  ( "proof" | ";" )*
  Reasoning "end" .
```

I am proposing we change the `( "proof" | ";" )` to just `"proof"`, i.e.,

```
Scheme-Block = "scheme" Scheme-Identifier "{" Scheme-Parameters "}" ":"
  Scheme-Conclusion [ "provided" Scheme-Premise { "and" Scheme-Premise } ]
*  "proof"*
  Reasoning "end" .
```

...or even better...

```
Scheme-Block = "scheme" Scheme-Identifier "{" Scheme-Parameters "}" ":"
  Scheme-Conclusion [ "provided" Scheme-Premise { "and" Scheme-Premise } ]
*  Proof* .
```

This change adheres to the principle of least surprise: theorems require
either a justification or a `Proof` as a justification, schemes should have
a similar structure (but only `Proof` makes sense, really).

Only two schemes currently do not adhere to this proposed syntax (one in
FIELD_16, another in PRE_CIRC).

And the change requires only minimal changes to the parser.

Best,
Alex

--0000000000005c99020648472b42
Content-Type: text/html; charset="UTF-8"
Content-Transfer-Encoding: quoted-printable

<div dir=3D"ltr">Hello,<br><br>Right now, the syntax for a scheme looks lik=
e:<div><br></div><div>```</div><div><font face=3D"monospace">Scheme-Block =
=3D &quot;scheme&quot; Scheme-Identifier &quot;{&quot; Scheme-Parameters &q=
uot;}&quot; &quot;:&quot;<br>=C2=A0 Scheme-Conclusion [ &quot;provided&quot=
; Scheme-Premise { &quot;and&quot; Scheme-Premise } ]<br><b>=C2=A0 ( &quot;=
proof&quot; | &quot;;&quot; )</b><br>=C2=A0 Reasoning &quot;end&quot; .</fo=
nt></div><div>```</div><div><br></div><div>I am proposing we change the `<f=
ont face=3D"monospace">( &quot;proof&quot; | &quot;;&quot; )</font>` to jus=
t `<font face=3D"monospace">&quot;proof&quot;</font>`, i.e.,</div><div><br>=
</div><div>```</div><div><font face=3D"monospace">Scheme-Block =3D &quot;sc=
heme&quot; Scheme-Identifier &quot;{&quot; Scheme-Parameters &quot;}&quot; =
&quot;:&quot;<br>=C2=A0 Scheme-Conclusion [ &quot;provided&quot; Scheme-Pre=
mise { &quot;and&quot; Scheme-Premise } ]<br><b>=C2=A0 &quot;proof&quot;</b=
><br>=C2=A0 Reasoning &quot;end&quot; .</font></div><div>```</div><div><br>=
</div><div>...or even better...</div><div><br></div><div><div>```</div><div=
><font face=3D"monospace">Scheme-Block =3D &quot;scheme&quot; Scheme-Identi=
fier &quot;{&quot; Scheme-Parameters &quot;}&quot; &quot;:&quot;<br>=C2=A0 =
Scheme-Conclusion [ &quot;provided&quot; Scheme-Premise { &quot;and&quot; S=
cheme-Premise } ]<br><b>=C2=A0 Proof</b>=C2=A0.</font></div><div>```</div><=
/div><div><br></div><div>This change adheres to the principle of least surp=
rise: theorems require either a justification or a `<font face=3D"monospace=
">Proof</font>` as a justification, schemes should have a similar structure=
 (but only `<font face=3D"monospace">Proof</font>` makes sense, really).</d=
iv><div><br></div><div>Only two schemes currently do not adhere to this pro=
posed syntax (one in FIELD_16, another in PRE_CIRC).<br><br>And the change=
=C2=A0requires only minimal changes to the parser.<br><br>Best,<br>Alex</di=
v></div>

--0000000000005c99020648472b42--