Stream: Isabelle/ML

Topic: syntax engine

view this post on Zulip HuanSun (Jan 27 2022 at 14:23):

I'm attempting to understand Isabelle's inner syntax engine, but I'm having problems reading Chapter 8 of the Isabelle standard reference manual. (Isar-ref or [The Isabelle/Isar Reference Manual][1] by Makarius Wenzel).

As seen in the diagram below, there is a general inner syntax engine described in the manual. I'm trying to figure out how this process works and where functions like syntax translation print_translation come into play in this diagram.

[![enter image description here][2]][2]

Furthermore, is there a simple example for learning this entire process?


Last updated: Mar 04 2024 at 12:30 UTC