Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] name of locale predicate


view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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: Mar 29 2024 at 08:18 UTC