*From: *Waqar Ahmad <12phdwah...@seecs.edu.pk>
> *Date: *Thursday, 9 August 2018 at 06:08
> *To: *"Norrish, Michael (Data61, Acton)"
> *Cc: *hol-info
> *Subject: *Re: [Hol-info] Partial Function on lazy list
>
>
>
> Hi,
>
>
>
> Great!. This reall
; it looks too much like a name for
a predicate. You should use a name like ‘e’ instead.
Michael
From: Waqar Ahmad <12phdwah...@seecs.edu.pk>
Date: Thursday, 9 August 2018 at 06:08
To: "Norrish, Michael (Data61, Acton)"
Cc: hol-info
Subject: Re: [Hol-info] Partial Function on lazy
ap (SIMP_RULE bool_ss [GSYM until_def])
>[until0_FNIL, until0_FCONS])
> - -
>
> Michael
>
>
>
> From: Waqar Ahmad via hol-info
> Reply-To: Waqar Ahmad <12phdwah...@seecs.edu.pk>
> Date: Tuesday, 7 August 2018 at 03:26
&
until P ll = until0 P (F, ll)’
val until_thm = LIST_CONJ (map (SIMP_RULE bool_ss [GSYM until_def])
[until0_FNIL, until0_FCONS])
- -
Michael
From: Waqar Ahmad via hol-info
Reply-To: Waqar Ahmad <12phdwah...@seecs.edu.pk>
Date: Tuesday, 7 August 2018 at 03:26
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
