Stream: Beginner Questions

Topic: Infix syntax


view this post on Zulip Hamed Hajisadeghian (Sep 19 2021 at 18:30):

What is the general form of defining infix syntax? What is the meaning of numbers and brackets([]) in this example?

datatype com = SKIP
  |Assign vname aexp        ("_ ::= _" [1000, 61] 61)
  |Seq com com              ("_ ;;/ _" [60, 61] 60)
  |If bexp com com          ("(IF _/ THEN _/ ELSE _)" [0, 0, 6] 61)
  |While bexp com           ("(WHILE _/ DO _)" [0, 61] 61)

Thanks for your answer.

view this post on Zulip Robert Soeldner (Sep 19 2021 at 18:33):

You can read about the mixfix notation in the Isar-Ref, Chapter 8.2 https://isabelle.in.tum.de/doc/isar-ref.pdf


Last updated: Jul 15 2022 at 23:21 UTC