[isabelle] HOL.default typeclass?



Hi all,

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?


--
  Peter





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