(* Title: Deriving class instances for datatypes Author:ChristianSternagelandRenéThiemann<christian.sternagel|rene.thiemann@uibk.ac.at> Maintainer:ChristianSternagelandRenéThiemann License:LGPL
*) section‹Loading Existing Derive-Commands› theory Derive imports "Comparator_Generator/Compare_Instances" "Equality_Generator/Equality_Instances" "Hash_Generator/Hash_Instances" "Countable_Generator/Countable_Generator" begin
text‹
just load the commands to derive comparators, equality-functions, hash-functions, and the
to show that a datatype is countable, so that now all of them are available.
are further generators available in the AFP entries Containers and Show. ›
print_derives
end
Messung V0.5 in Prozent
¤ Dauer der Verarbeitung: 0.10 Sekunden
(vorverarbeitet am 2026-06-10)
¤
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung und die Messung sind noch experimentell.