Re: [isabelle] List construction
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"
> "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".)
This archive was generated by a fusion of
Pipermail (Mailman edition) and