Tobias On 08/06/2015 16:43, Lars Noschinski wrote:
On 08.06.2015 16:34, Jasmin Blanchette wrote:The rule âXâ appears to violate the golden rule of thumb when using âsimpâ, i.e. that both the rhs and the preconditions should be simpler than the lhs (see Section 2.5.3 of Concrete Semantics). Surely, âf x ~= aâ is not simpler than âf xâ. That bad things happen then doesnât surprise me so muchâ Cheers, JasminIt is only simpler insofar as that it is literally part of the assumptions. I would not have been surprised if the simplifier had started looping -- after all, it is not really simpler. But refusal to rewrite does not yet fit into my mental model of the simplifier.
Description: S/MIME Cryptographic Signature