From 90149982a973c9255d04c96ffed793e660e0065a Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Tam=C3=A1s=20T=C3=B3th?= Date: Thu, 16 Jan 2025 00:02:20 +0100 Subject: [PATCH] Update `kore-syntax.md` with multiary `\and` syntax (#4086) Reflects the changes of #3666 in `kore-syntax.md`. --- docs/kore-syntax.md | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) 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