Email Gateway (Aug 18 2022 at 15:14): Email Gateway (Aug 18 2022 at 15:14):From: Christian Sternagel <christian.sternagel@uibk.ac.at>
Hi,
if I understood correctly, for every locale of name "L" we get a
predicate of name "L" taking the fixes of the locale as argument. Is it
possible to influence the name of this predicate?
cheers
chris
Email Gateway (Aug 18 2022 at 15:15):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Christian,
on the ML level this is possible; however there is no Isar syntax for
this. What is your scenario? The illusion of a differently named
locale predicate can be created using an abbreviation.
Hope this helps,
Florian
signature.asc
Email Gateway (Aug 18 2022 at 15:15):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Christian,
this problem will disappear in the next Isabelle release: we introduced
mandatory prefixes for locale predicates stemming from classes ;-)
Florian
signature.asc
Email Gateway (Aug 18 2022 at 15:15):From: Christian Sternagel <christian.sternagel@uibk.ac.at>
I have a type class that is essentially the same as Haskell's Show
class. Hence I wanted to name it show, but then I can not define a
function named 'show' (for showing a string) inside the class. Currently
I'm using to_string instead of show, but I thought it would be nice to
have the same naming as in Haskell :)
cheers
chris
Last updated: Nov 21 2024 at 12:39 UTC