Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Minor bug in output from "locale" with notation


view this post on Zulip Email Gateway (Aug 22 2022 at 17:21):

From: "Eugene W. Stark" <isabelle-users@starkeffect.com>
In Isabelle 2017, if I load the theory:

theory Barf
imports Main
begin

locale L =
fixes X :: "'x ⇒ 'x ⇒ 'x" (infixr "⋅" 55)

end

and then put the mouse over the locale definition, I see the following
in the output window:

locale

L

fixes X :: "'x ⇒ 'x ⇒ 'x" (infixl "⋅" 55)

That is, it seems to output the fixity incorrectly.

view this post on Zulip Email Gateway (Aug 22 2022 at 17:21):

From: Makarius <makarius@sketis.net>
The output is indeed incorrect. There are a few more oddities in the
formatting and the defaults for other mixfix annotations.

I will improve this for the coming release -- presumably published in
August 2018.

Makarius


Last updated: Nov 21 2024 at 12:39 UTC