Re: [isabelle] disabling datatype syntax



On Sun, Feb 22, 2009 at 11:21, Chris Capel <pdf23ds at gmail.com> wrote:
> Is there a way to temporarily enable/disable syntax declared on
> datatype constructors? I assume it would be done with no_syntax or
> no_translations, but I'm not sure how.
>
> I just tried a no_translations declaration, and that didn't seem to
> work. I'm not sure what the no_syntax declaration would look like. The
> only line that appears relevant from running isar-help-syntax is
>
> logic = "!(" logic[0] => "Start" (80)

Ahh, I see. You have to treat the constructor as a constant
declaration. So in my case,

no_syntax Start :: "nat => token" ("!'(_" 80)

Chris Capel
-- 
"What is it like to be a bat? What is it like to bat a bee? What is it
like to be a bee being batted? What is it like to be a batted bee?"
-- The Mind's I (Hofstadter, Dennet)





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