[isabelle] one function for two datatypes
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 !
This archive was generated by a fusion of
Pipermail (Mailman edition) and