Commit 7b01f7babb92f9a7af62d0ac2d99f1ae67d0ca2b - Eqthy

Raise error if naming theorem or axiom with already existing name. Chris Pressey 3 months ago

5 changed file(s) with 14 addition(s) and 3 deletion(s). Raw diff Collapse all Expand all

-0

HISTORY.md less more

8	8
9	9	0.5
10	10	---
	11
	12	Language:
	13
	14	* It is not valid to name a theorem or an axiom with the
	15	same name as an existing theorem or axiom.
11	16
12	17	Implementation:
13	18

-1

README.md less more

116	116
117	117	* Allow the first line of a proof to be an axiom.
118	118	* Arity checking in parser would prevent some silly errors in axioms.
119		* Prevent naming a theorem or axiom with a name already in context.
	119	* Improve unnamed theorem and axiom support (unique names across files.)
120	120
121	121	### Desired Examples
122	122

-1

eg/absorption-laws.eqthy.md less more

-1

eg/boolean-algebra.eqthy.md less more

190	190	not(0) = 1
191	191	qed
192	192
193		theorem
	193	theorem (#comp-involutive)
194	194	not(not(A)) = A
195	195	proof
196	196	and(or(not(not(A)), A), 1) = and(or(not(not(A)), A), 1)

-0

src/eqthy/verifier.py less more

11	11	Term, Eqn, RewriteRule,
12	12	all_rewrites, render, replace, apply_substs_to_rule
13	13	)
	14
	15
	16	class NamingError(Exception):
	17	pass
14	18
15	19
16	20	class DerivationError(Exception):

28	32
29	33	def register(self, name: str, lhs: Term, rhs: Term) -> None:
30	34	self.log("Registering rule [{}]: {} = {}", render(name), render(lhs), render(rhs))
	35	if (name + '_1') in self.rules:
	36	raise NamingError("The name '{}' has already been defined".format(name))
31	37	self.rules[name + '_1'] = RewriteRule(pattern=lhs, substitution=rhs)
32	38	self.rules[name + '_2'] = RewriteRule(pattern=rhs, substitution=lhs)
33	39