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.


> On 22.03.2015, at 12:00, lyj238 at 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


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.