Email Gateway (Oct 27 2024 at 18:57): Email Gateway (Oct 27 2024 at 18:57):From: Peter Lammich <cl-isabelle-users@lists.cam.ac.uk>
Dear list,
is there a 'safe' way to declare a new type that is member of a type-class.
For example
typedecl my_type :: countable?
By safe, I mean something that does not involve axiomatizing the
type-class constraints.
The best I can currently come up with is:
typedecl mytype
axiomatization my_to_nat :: "mytype ⇒ nat"
where inj_my_to_nat: "inj my_to_nat"
instance mytype::countable
apply standard
using inj_my_to_nat by blast
I assume that is safe as long as the type-class is inhabited?
--
Peter
Last updated: Jan 04 2025 at 20:18 UTC