Email Gateway (Aug 19 2022 at 17:15): Email Gateway (Aug 19 2022 at 17:15):From: "W. Douglas Maurer" <maurer@gwu.edu>
After receiving Florian Haftmann's helpful response to my problem
with \<emptyset>, I decided to try to extend this to be able to work
with \<int> (the Z in a special font that means the set of all
integers). There is a button for this under Letter in the Symbols
pane. Accordingly, just like the use of notation Set.empty
("\<emptyset>"), I tried notation Int.int ("\<int>"). The \<int> came
out properly on the screen as the Z in a special font. Then I tried
using it. If I write lemma "(a<(b::int))\Longrightarrow (a+c<b+c) by
simp, that works. But if I substitute \<int> for int in the above,
then \<int> again comes out on the screen as the Z in a special font,
but the proof doesn't go through. I tried replacing Int.int in the
notation statement by just int, but that doesn't work either. I
suspect that there is something wrong with Int.int, but I don't know
what syntax to try next.
Email Gateway (Aug 19 2022 at 17:15):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Hi,
Isabelle has separate syntax and commands for terms and types. To change the notation for
types, use the command type_notation instead of notation. In your particular case with
int, the notation command did not complain, because there is also the function Int.int
(which converts natural numbers into integers).
Hope this helps,
Andreas
Email Gateway (Aug 19 2022 at 17:16):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
\<^bsub> and \<^esub> cannot be part of the name of an identifier (variable, function,
constant, ...), they are meant to be used for subscripting terms in mixfix syntax. If you
want to have subscripts for identifiers, you must stick to \<^sub>. If the index consists
of several letters, each must carry its own \<^sub> as in x\<^sub>1\<^sub>2. Conversely,
when you define your own syntax for a function in which terms are subscripted, only use
\<^bsub> and \<^esub>, but not \<^sub>. Otherwise, you will get strange effects.
Hope this helps,
Andreas
Last updated: Apr 20 2024 at 01:05 UTC