CODEWITHSUNDEEP
latexisabelle
Nadezhda Baklanova
Nadezhda Baklanova

Reputation: 97

How to print type definitions to Latex from Isabelle?

I'm using Isabelle document preparation for generating tex files. I wonder if there is an antiquotation for datatype definition so that it would be fully printed in latex.

In some file there is a definition

datatype t = A nat | B bool

And later I want to print this definition to latex. I didn't find any way how to do it in the Isabelle docs.

An antiquotation @{datatype xyz} was mentioned in the Isabelle mailing list, but it doesn't work for me (Isabelle 2013-2).

Does anybody know about an appropriate antiquotation for type definitions?

Upvotes: 2

Views: 418

Answers (1)

davidg
davidg

Reputation: 6007

It seems to work for me in Isabelle 2013-2.

The Isabelle theory file:

theory Baz
imports Main
begin

datatype t = A nat | B bool

text {*
  @{datatype t}
*}

end

results in the document:

Output Isabelle Document

The first datatype is the definition, while the second is the display anti-quotation.

Perhaps the problem is that your @{datatype} anti-quotation isn't in a text {* ... *} block?

Upvotes: 4

Related Questions