Re: [isabelle] List construction



Oops...I read List.thy but I don't seen it.
Sorry.

Thanks
Gabriele

On 10/4/06, Tjark Weber <tjark.weber at gmx.de> wrote:

Gabriele,

On Tuesday 03 October 2006 17:32, Gabriele Pozzani wrote:
> I'm writing a function to contruct a list of given length.
>
> I defined a datatype:
> datatype resource = free | taken
>
>  and the function:
> emptyRes2aux :: "unit => nat => resource list"
> primrec
> "emptyRes2aux () (k) = (case k of 0 => [] | Suc h => free # emptyRes2aux
() h)"

what you want to define seems to be equal to

  replicate n free

(See HOL/List.thy for the definition of "replicate".)

Best,
Tjark





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