Email Gateway (Aug 18 2022 at 14:06): Email Gateway (Aug 18 2022 at 14:06):From: Steven Obua <obua@wjpserver.cs.uni-sb.de>
Hi,
I want to convert some Isabelle 2007 stuff to Isabelle 2009. I
encountered problems with this:
datatype float = Float int int
instance float :: zero
Zero_float_def: "0 \<equiv> Float 0 0" ..
How do I write this the Isabelle 2009 way? Any quick idea?
Steven Obua
Email Gateway (Aug 18 2022 at 14:07):From: Johannes Hölzl <hoelzl@in.tum.de>
An updated version of our Floating-Point library is already available:
import "~~/src/HOL/Library/Float"
or:
instantiation float :: zero begin
definition zero_float where "0 = Float 0 0"
instance ..
end
Johannes
Email Gateway (Aug 18 2022 at 14:07):From: Andreas Lochbihler <lochbihl@ipd.info.uni-karlsruhe.de>
Hi Steven,
type class instantiation where parameters must be defined now use
explicitly the definition command (without the "where" clause):
instantiation float :: zero begin
definition Zero_float_def: "0 \<equiv> Float 0 0"
instance ..
end
Regards,
Andreas
Steven Obua schrieb:
Email Gateway (Aug 18 2022 at 14:07):From: Christian Sternagel <christian.sternagel@uibk.ac.at>
This should do it.
instantiation float :: zero begin
definition Zero_float_def: "0 = Float 0 0"
instance ..
end
see also HOL/Library/Float.thy.
cheers
chris
Email Gateway (Aug 18 2022 at 14:07):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Steven,
the explanation can be found at
http://isabelle.in.tum.de/repos/isabelle/file/5c8618f95d24/src/HOL/Library/Float.thy
or in the class tutorial among the Isabelle documentation.
Hope this helps
Florian
signature.asc
Last updated: Apr 19 2024 at 20:15 UTC