Re: [isabelle] flat function exists in Isabelle lib?
find_consts "'a list list â 'a list"
found 4 constant(s):
List.product_lists :: "'a list list â 'a list list"
List.transpose :: "'a list list â 'a list list"
List.transpose_sumC :: "'a list list â 'a list list"
List.concat :: "'a list list â 'a listâ
concat  = 
concat (?x # ?xs) = ?x @ concat ?xs
List.concat is the one your want.
> On 22.03.2015, at 12:00, lyj238 at ios.ac.cn wrote:
> Dear all:
> I need a flat function, which can be explained bya small example:
> flat [[1,2],[2,3],[5,4]]=[1,2,3,5,4];
> Its Intuitive meaning:
> flaten a list of list into a list?
> Is there such a function flat in Isabelle's library.
> I have tried to find, but fail?
> Need I define it by myself?
> lyj238 at ios.ac.cn
The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.
This archive was generated by a fusion of
Pipermail (Mailman edition) and