CODEWITHSUNDEEP
isabelle
thor
thor

Reputation: 22460

How to write isabelle iterated implications in ASCII

While learning Isabelle (2020), I tried to copy an example from its documentation (PDF) into a .thy file, which contains an iterated implication. Since the documentation is in PDF, I don't know what the correct ASCII for it should be. The closest I can get is this:

lemma "[[ xs @ ys = ys @ xs ; length xs = length ys]]   ==> xs = ys"

But Isabelle complains about an "Inner Syntax error". I tried to use "[...;...]", but Isabelle seems to be treating it as a list, and complains about clashing between list and bool.

How should one type the formula in ASCII?

In general, how does one find the ASCII for notation from the PDF documentation? Is there a look-up table somewhere?

Upvotes: 0

Views: 186

Answers (1)

Manuel Eberl
Manuel Eberl

Reputation: 8258

The name of these symbols is \<lbrakk> and \<rbrakk>. The corresponding Unicode characters are ⟦ and ⟧. If you type [| or |] in Isabelle/jEdit, it will automatically get converted to these.

Copying code out of PDFs almost never works; PDF is a pretty horrible format.

One good place to find symbols is the ‘Symbols’ tab in Isabelle/jEdit. You can e.g. find these brackets in the ‘Punctuation’ section. There is also the ~~/etc/symbols file, but I don't think that is very helpful for this case because it only shows the Unicode codepoint, but not the character itself.

Upvotes: 2

Related Questions