Re: [isabelle] Why doesn't \<emptyset> work? (W. Douglas Maurer)



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

On 18/02/15 00:51, W. Douglas Maurer wrote:
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.




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.