Skip to content

Commit

Permalink
Update kore-syntax.md with multiary \and syntax (#4086)
Browse files Browse the repository at this point in the history
Reflects the changes of #3666 in `kore-syntax.md`.
  • Loading branch information
tothtamas28 authored Jan 15, 2025
1 parent 9493430 commit 9014998
Showing 1 changed file with 5 additions and 5 deletions.
10 changes: 5 additions & 5 deletions docs/kore-syntax.md
Original file line number Diff line number Diff line change
Expand Up @@ -187,8 +187,8 @@ A sort is either a _sort variable_ or a _sort constructor_ applied to a list of
"\top" "{" <sort> "}" "(" ")"
| "\bottom" "{" <sort> "}" "(" ")"
| "\not" "{" <sort> "}" "(" <pattern> ")"
| "\and" "{" <sort> "}" "(" <pattern> "," <pattern> ")"
| "\or" "{" <sort> "}" "(" <pattern> "," <pattern> ")"
| "\and" "{" <sort> "}" "(" <patterns> ")"
| "\or" "{" <sort> "}" "(" <patterns> ")"
| "\implies" "{" <sort> "}" "(" <pattern> "," <pattern> ")"
| "\iff" "{" <sort> "}" "(" <pattern> "," <pattern> ")"
// Quantifiers
Expand All @@ -213,10 +213,10 @@ A sort is either a _sort variable_ or a _sort constructor_ applied to a list of
| "\right-assoc" "{" "}" "(" <application-pattern> ")"
```

The left-assoc (resp. right-assoc) construct allows a chain of applications of
The `left-assoc` (resp. `right-assoc`) construct allows a chain of applications of
left associative (resp. right associative) binary symbols to be flattened.
For example (simplified), `\and(\and(P1, P2), P3)` can be represented as
`\left-assoc(\and(P1, P2, P3))`.
For example, `foo(foo(P1, P2), P3)` can be represented as
`\left-assoc(foo(P1, P2, P3))`.

### Attributes

Expand Down

0 comments on commit 9014998

Please sign in to comment.