No, there are known problems here unfortunately. See our github issue about it ( https://github.com/mn200/HOL/issues/97 ) for some discussion.
As per my comment there, I’m inclined to go with changing the order of arguments to the case constants, and to then play parsing/printing tricks to retain backwards compatibility. Michael On 14/11/12 09:33, Vincent Aravantinos wrote: > Hi, > > I played a little bit with computeLib in order to see its capabilities > and got stuck with efficiency problems when dealing with "case ... of". > My problem is that all branches are necessarily evaluated thus yielding > huge efficiency wastes. > The standard way to control the evaluation order for parameters would be > lazyfy_thm. > However, it is of no use here since the argument which allows to decide > on which branch to follow is the last one. > For instance ``case x of T => 1 | F => 2`` is actually a shortcut for > ``bool_case 1 2 x``: x is in the end so lazyfy_thm cannot do anything. > > Did I misunderstand something or is there a standard workaround? > > Regards, >
signature.asc
Description: OpenPGP digital signature
------------------------------------------------------------------------------ Monitor your physical, virtual and cloud infrastructure from a single web console. Get in-depth insight into apps, servers, databases, vmware, SAP, cloud infrastructure, etc. Download 30-day Free Trial. Pricing starts from $795 for 25 servers or applications! http://p.sf.net/sfu/zoho_dev2dev_nov
_______________________________________________ hol-info mailing list [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
