*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] one function for two datatypes*From*: Manuel Eberl <eberlm at in.tum.de>*Date*: Sat, 03 Aug 2013 02:18:44 +0200*In-reply-to*: <178406BB-F87D-4F58-983A-16B367844FC3@loria.fr>*References*: <178406BB-F87D-4F58-983A-16B367844FC3@loria.fr>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:17.0) Gecko/20130510 Thunderbird/17.0.6

Hallo, this is analogous to the approach taken in functional languages such as Haskell: you can define a type class (e.g. "getval") that defines a getval function of the appropriate type and then declare type class instances for your two datatypes. This way, you get something akin to overloading in Java. But let us not talk about the Java type system. If you don't know how to do use type classes in Isabelle, you can find lots of examples in the Isabelle theory library; off the top of my head, I vaguely remember something like this being done for a function extracting variables from boolean and arithmetic expressions in IMP, that could serve as an example. Of course, there is also the type class tutorial by Florian Haftmann: http://isabelle.in.tum.de/dist/Isabelle2013/doc/classes.pdf Regarding the second question, I'm not entirely sure if I understood that correctly, but if I have, the only way to do this that I can think of is also by incorporating a function that does this into the type class and then writing appropriate instances for your datatypes. Cheers, Manuel On 08/02/2013 11:21 PM, Henri DEBRAT wrote: > Hi all, > > > Let's say I have two datatypes: > > datatype 't t1 = C1a 't | C1b 't option > > datatype 't t2 = C2a 't | C2b 't option > > Then let's say that for a common 'y type, I have two elements e1 of type 'y t1 and e2 of type 'y t2. > > let us finally say there is a value v such that e1 = C1a v and e2 = C2a v. > > How could I define a "getval" function such that getval e1 = getval e2 is a admissible expression ? What type would it have ? It sounds like Java overloading, but I do not reckon there is such a thing in Isabelle, am I wrong ? > > Secondly, is there any way I could say that some element e, which type could be either t1 or t2, is such that getval e = Some v, without having to say wether C1b or C2b was used to define it ? > > Thanks in advance ! > H.

**References**:**[isabelle] one function for two datatypes***From:*Henri DEBRAT

- Previous by Date: [isabelle] one function for two datatypes
- Next by Date: Re: [isabelle] nothing important
- Previous by Thread: [isabelle] one function for two datatypes
- Next by Thread: Re: [isabelle] nothing important
- Cl-isabelle-users August 2013 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list