You need to define a helper function that has as its state not only the llist
that is being consumed but also a Boolean indicating whether or not to stop
(because a P-satisfying element has been seen).
- -
val until0_def =
new_specification ("until0_def", ["until0"],
ISPEC ``λbll. if
Hi all,
Is there any easy way to define the following partial function on lazy list
val recur_llist_fn_def = Define
`recur_llist_fn P w =
if P (THE (LHD w)) then [|THE (LHD w)|]
else (THE (LHD w)):::(recur_llist_fn P (THE (LTL w)))`;
Otherwise, I can also include the LNIL case as
val
Hi,
is the improved version you’re using available somewhere?
—Chun
> Il giorno 05 ago 2018, alle ore 18:09, Waqar Ahmad <12phdwah...@seecs.edu.pk>
> ha scritto:
>
> Hi Chun,
>
> I'm not sure about your potential conflict question but we are now using an
> improved definition of
Hi Thomas,
thanks for detailed explanations!
—Chun
> Il giorno 05 ago 2018, alle ore 19:58, Thomas Tuerk
> ha scritto:
>
> Hi Chun, Waqar,
>
> "Define" does indeed give priority to earlier clauses. Under the hood pattern
> compilation takes place. So what is actually is going on for
>> val
Call for Participation
11th Conference on Intelligent Computer Mathematics
- CICM 2018 -
August 13-17, 2018
RISC, Hagenberg, Austria
**
14th International Conference on integrated Formal Methods (iFM)
http://ifm2018.cs.nuim.ie
