Re: [isabelle] HOL.default typeclass?



Hi Peter,

> HOL defines a typeclass default. What is the purpose of that? The only
> instantiations are for unit (in Product_Type), and some instantiations
> for nat splattered around various sessions.
> 
> What I need is a typeclass that gives me an *executable* default value,
> is the default-typeclass the right one for that?

yes, it is.  The reason why the HOL theories are spare of instantiations
is to give the user as much freedom as possible.  The instantiation for
unit is an exception, for one obvious reason and one less obvious: sort
{default} being inhabited by one witness instance avoids problems with
pending sort hypotheses etc., particularly in code equations.

Cheers,
	Florian

-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

Attachment: signature.asc
Description: OpenPGP digital signature



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