On 30/10/17 16:16, michael.norr...@data61.csiro.au wrote:
> In these situations, the simplifier detects the potential loop and only
> rewrites if the resulting term is smaller than the original in some
> well-founded order.
Thanks.
--
Do not eat animals; respect them as you respect people.
htt
In these situations, the simplifier detects the potential loop and only
rewrites if the resulting term is smaller than the original in some
well-founded order.
Michael
On 31/10/17, 04:30, "Mario Castelán Castro" wrote:
On 29/10/17 16:18, michael.norr...@data61.csiro.au wrote:
> Passin
On 29/10/17 16:18, michael.norr...@data61.csiro.au wrote:
> Passing the theorem EQ_SYM_EQ will normalise this sort of thing:
Thanks.
Before your answer thought that would loop but it does not.
--
Do not eat animals; respect them as you respect people.
https://duckduckgo.com/?q=how+to+(become+OR
Passing the theorem EQ_SYM_EQ will normalise this sort of thing:
> EQ_SYM_EQ;
val it =
|- ∀x y. x = y ⇔ y = x:
thm
> SIMP_CONV (srw_ss()) [EQ_SYM_EQ] “a = b ∧ x = z ⇔ b = a ∧ x = z”;
<>
val it =
|- (a = b ∧ x = z ⇔ b = a ∧ x = z) ⇔ T:
thm
Michael
On 29/10/17, 02:58, "Mario Castelán C
Sometimes I have a goal of the form “P = Q” where P and Q are terms that
are the same except for the order of the arguments of a symmetric
relation, e.g. (in this case equality): “a = b ∧ x = z ⇔ b = a ∧ x = z”.
Can these sub-terms be normalized by SIMP_TAC analogous to how it can
normalize associ
