Email Gateway (Aug 19 2022 at 08:33): Email Gateway (Aug 19 2022 at 08:33):From: Tobias Nipkow <nipkow@in.tum.de>
by René Thiemann
We provide a tactic which automatically synthesizes linear orders for datatypes
as it is possible using Haskell's ``deriving Ord'' feature. The tactic is able
to handle datatypes with mutual or higher-order recursion, if the nesting is not
too complex.
Our method complements the Isabelle Collection Framework which for some
datastructures---like balanced trees---demands that the type of keys is linearly
ordered.
Our formalization was performed as part of the IsaFoR/CeTA project. With our new
tactic we could completely remove tedious proofs for linear orders of two datatypes.
http://afp.sourceforge.net/entries/Datatype_Order_Generator.shtml
Scrap your boilerplate!
And enjoy.
Last updated: Apr 23 2024 at 08:19 UTC