Re: [isabelle] Multiset ordering vs. subset syntax



It would be great to get some feedback from the mailing list as to who would be affected by this change.

Existing users of multiset orderings, please speak up!

If hardly anybody is going to be affected, then the change should be implemented in full for the next release.

Larry

> On 1 Apr 2015, at 16:03, Jasmin Blanchette <jasmin.blanchette at inria.fr> wrote:
> 
> Hi all,
> 
>> I am not sure whether it would be best to do the swap in one step.
> 
> Actually, Florianâs email made me rethink about this, and maybe as many as three steps will be necessary (leading us to Isabelle2016-1 or Isabelle2017):
> 
> 1. Rename <# etc. to #<# (or whatever odd syntax).
> 2. Rename < and \<subset> to <# and \<subset>#.
> 3. Rename #<# to <.
> 
> My goal is to maximize the number of cases where changes trigger clear errors when processing theories, and minimize subtle change of semantics. Even in a theorem prover, semantic changes can be difficult to debug. Combining steps 2 and 3 would lead to some confusion â a term like âA < Bâ would suddenly change semantics, without giving an immediate error.
> 
> Anyway, we will see. For the moment, if there are no voices against my implementing step 1, I will go ahead (e.g. next week).
> 
> Thanks to all for your feedback!
> 
> Jasmin
> 
> 





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.