Re: [isabelle] Using timeLimit with tactics



On Saturday 19 May 2012 13:43:17 Tjark Weber wrote:
> loop_tac is a curried function that takes two arguments. With the second
> grouping, timeLimit limits the runtime of partially applying loop_tac to
> one argument (@{context}). But this partial application (which yields
> loop_tac @{context}, a function of one argument) takes (almost) no time
> anyway.
> 
> Infinite recursion happens once you apply loop_tac @{context} to an
> argument (i.e., 1). But with the second grouping, this application is no
> longer guarded by timeLimit.

Yup, thanks. I guess the auto_tac timeout after 50ms stems from evaluating the 
@{context} and whatever it is that mk_auto_tac does. However I probably 
wouldn't have gotten the whole Seq and SINGLE thing to eagerly everything 
properly without Jasmin's help.

Best,
Ognjen





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