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.

You can read about the `mixfix`

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

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

Hamed Hajisadeghian has marked this topic as resolved.

Last updated: Dec 07 2023 at 08:19 UTC