diff --git a/docs/kore-syntax.md b/docs/kore-syntax.md index ff1d9b30d8..c4f198f9dd 100644 --- a/docs/kore-syntax.md +++ b/docs/kore-syntax.md @@ -187,8 +187,8 @@ A sort is either a _sort variable_ or a _sort constructor_ applied to a list of "\top" "{" "}" "(" ")" | "\bottom" "{" "}" "(" ")" | "\not" "{" "}" "(" ")" - | "\and" "{" "}" "(" "," ")" - | "\or" "{" "}" "(" "," ")" + | "\and" "{" "}" "(" ")" + | "\or" "{" "}" "(" ")" | "\implies" "{" "}" "(" "," ")" | "\iff" "{" "}" "(" "," ")" // Quantifiers @@ -213,10 +213,10 @@ A sort is either a _sort variable_ or a _sort constructor_ applied to a list of | "\right-assoc" "{" "}" "(" ")" ``` -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