CODEWITHSUNDEEP
syntaxisabelle
TomR
TomR

Reputation: 3056

Trying to understand "syntax" keyword in Isabelle/HOL

I am trying to understand implementation of Linear logic in Isabelle/HOL: https://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/library/Sequents/Sequents/ILL.html For what does syntax keyword stand for, what is meant by code:

syntax
  "_Trueprop" :: "single_seqe" ("((_)/ ⊢ (_))" [6,6] 5)
  "_Context"  :: "two_seqe"   ("((_)/ :=: (_))" [6,6] 5)
  "_PromAux"  :: "three_seqe" ("promaux {_||_||_}")

Where can I find documentation for the syntax keyword? I have found exhaustive documentation about infixr and translation rules in Lecture Notes in Computer Science Vol 828. But I can not find similar documentation about syntax.

Upvotes: 0

Views: 136

Answers (1)

Rupert Swarbrick
Rupert Swarbrick

Reputation: 21

This is described in the reference manual in section 8.5.2 (as of Isabelle 2016-1): "Raw syntax and translations".

The first line there means to add a syntax rule saying that P ⊢ Q parses to _Trueprop P Q. The next lines of ILL.thy give a parse_translation, described just afterwards in the same section of the reference manual. This translation tells Isabelle to translate _Trueprop to K (single_tr Trueprop) and Trueprop is declared as an uninterpreted constant at the top of the file. You'll see there's also a print_translation, which controls the pretty printer.

Upvotes: 2

Related Questions