Re: [isabelle] flatten of tuples

Personally, I would try to model values in your example using the hereditarily finite sets, as illustrated in my recent AFP paper and entry:


AFP entry:

Into this one type, you can naturally embed integers, booleans, characters, rationals, along with lists and trees built over them. You can also embed floating-point numbers, but not real numbers. Possibly that would be enough for your purposes. In the development version of the AFP, Iâve installed a file that defines a new type class, finitary, of types equipped with an embedding into HF. This is open-ended, because anything that is essentially a finite construction can be represented by a hereditarily finite set.

Larry Paulson

> On 27 Feb 2015, at 14:20, Viorel Preoteasa <viorel.preoteasa at> wrote:
> These programs are supposed to work with variables of different types
> mixed together (real, int, nat, bool). I can create a super type of them
> but then the verification of these programs will become more complicated.
> Lists are also not good because I could no longer encode in the type the
> number
> of arguments a program expects as input.

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