Side specs "on LHS", "on RHS" in hints are correctly handled.
Chris Pressey
3 months ago
11 | 11 |
|
12 | 12 |
Implementation:
|
13 | 13 |
|
|
14 |
* "on LHS", "on RHS" in hints are correctly handled.
|
14 | 15 |
* Correct line number is now reported in error messages when
|
15 | 16 |
the source Eqthy document is embedded in Markdown.
|
16 | 17 |
|
114 | 114 |
|
115 | 115 |
### Small Items
|
116 | 116 |
|
117 | |
* Tests for handling "on LHS", "on RHS" correctly in hints.
|
118 | 117 |
* Allow the first line of a proof to be an axiom.
|
119 | 118 |
* Arity checking in parser would prevent some silly errors in axioms.
|
120 | 119 |
* Test for error if naming a theorem or axiom with a name already in context.
|
339 | 339 |
qed
|
340 | 340 |
===> ok
|
341 | 341 |
|
|
342 |
A hint that names an axiom can also be specific about what side the
|
|
343 |
axiom is to be applied on.
|
|
344 |
|
|
345 |
axiom (idright) mul(A, e) = A
|
|
346 |
axiom (idleft) mul(e, A) = A
|
|
347 |
axiom (assoc) mul(A, mul(B, C)) = mul(mul(A, B), C)
|
|
348 |
theorem
|
|
349 |
A = mul(A, e)
|
|
350 |
proof
|
|
351 |
A = A
|
|
352 |
A = mul(A, e) [by idright on RHS]
|
|
353 |
qed
|
|
354 |
===> ok
|
|
355 |
|
|
356 |
If a hint names a side, it needs to be the correct side.
|
|
357 |
|
|
358 |
axiom (idright) mul(A, e) = A
|
|
359 |
axiom (idleft) mul(e, A) = A
|
|
360 |
axiom (assoc) mul(A, mul(B, C)) = mul(mul(A, B), C)
|
|
361 |
theorem
|
|
362 |
A = mul(A, e)
|
|
363 |
proof
|
|
364 |
A = A
|
|
365 |
A = mul(A, e) [by idright on LHS]
|
|
366 |
qed
|
|
367 |
???>
|
|
368 |
|
342 | 369 |
Naming an axiom in a hint when the axiom used was not actually used there
|
343 | 370 |
is incorrect. It is reasonable to (at least) warn the user of this mistake.
|
344 | 371 |
|