Re: [isabelle] Subtyping



-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA1

On 24/08/11 11:03, John Munroe wrote:
> 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.

It sounds like you might want to use a sum type, so that the type "'p"
is "'a + 'b".  There was a discussion about this quite recently on this
very list, starting here: http://tinyurl.com/3jzx3ny

Then you could have something like "f p = \<exists> a. p = Inl a" (but I
haven't tested this).

Tim
<><
-----BEGIN PGP SIGNATURE-----
Version: GnuPG v1.4.10 (GNU/Linux)
Comment: Using GnuPG with Mozilla - http://enigmail.mozdev.org/

iEYEARECAAYFAk5UZHMACgkQ/cBxZIxl6rmwnACfdWxXr+HPTl/8EOuAg0Y6j1Ai
378An1HvQucFMwMdkCUv4a+PtWuAXzbO
=Z7Ie
-----END PGP SIGNATURE-----





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