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â

thm concat.simps

  concat [] = []
  concat (?x # ?xs) = ?x @ concat ?xs

List.concat is the one your want.

Cheers,
Gerwin


> 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?
>
> regards!
>
>
>
>
>
> 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 MHonArc.