Stream: Beginner Questions

Topic: ✔ Infix syntax

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.

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

Hamed Hajisadeghian (Sep 19 2021 at 19:20):

Robert Soeldner said:

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

Thanks

Notification Bot (Sep 19 2021 at 19:20):

Hamed Hajisadeghian has marked this topic as resolved.

Last updated: Dec 21 2024 at 16:20 UTC