[isabelle] Subtyping



Hi,

I'm trying to define a function 'f' such that when the input is of
type 'A' it gives true, but when it's of type 'B' it gives false:
Would I need to make A and B subtypes of some parent type, say, 'P',
and that 'f' is of type "P => bool"? I can't seem to find much
documentation on subtyping.

If I use type classes instead:

class P
classes A < P
B < P

I can't seem to define the type of 'f' in terms of neither A, B, or P.

Any help on this will be much appreciated!

Thanks

John





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