Email Gateway (Aug 19 2022 at 11:18): Email Gateway (Aug 19 2022 at 11:18):From: Peter Lammich <lammich@in.tum.de>
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?
Email Gateway (Aug 19 2022 at 11:18):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Peter,
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
signature.asc
Last updated: Apr 23 2024 at 20:15 UTC