From 597cb3f00e6114667a86fbaf3ccb077a46760c79 Mon Sep 17 00:00:00 2001 From: Jaroslav Tulach Date: Thu, 14 Sep 2023 09:47:41 +0200 Subject: [PATCH] Removing notes on \ --- docs/syntax/types.md | 2 -- docs/types/hierarchy.md | 4 +--- 2 files changed, 1 insertion(+), 5 deletions(-) diff --git a/docs/syntax/types.md b/docs/syntax/types.md index b680e066f2a8c..4964f1467f702 100644 --- a/docs/syntax/types.md +++ b/docs/syntax/types.md @@ -87,7 +87,6 @@ working with types. These are listed below. | `;` | `< :`, `> =` | -2 | Left | Concatenates the left and right operand typesets to create a new typeset. | | `\|` | `> <:`, `> !`, `> in`, `> :` | 5 | Left | Computes the union of the left and right operand typesets. | | `&` | `> \|` | 6 | Left | Computes the intersection of the left and right operand typesets. | -| `\` | `> &` | 7 | Left | Computes the subtraction of the right typeset from the left typeset. | | `:=` | `< :`, `> =`, `> ;` | -1 | Left | Creates a typeset member by assigning a value to a label. | @@ -108,7 +107,6 @@ bind (`=`) has a relative level of -3 in this ordering. (declare-fun tsConcat () Int) ; `;` (declare-fun tsUnion () Int) ; `|` (declare-fun tsInter () Int) ; `&` -(declare-fun minus () Int) ; `\` (declare-fun tsMember () Int) ; `:=` (assert (> ascrip bind)) diff --git a/docs/types/hierarchy.md b/docs/types/hierarchy.md index 8dd5d7cbd4614..9b119bec5921a 100644 --- a/docs/types/hierarchy.md +++ b/docs/types/hierarchy.md @@ -194,10 +194,8 @@ They are as follows: product types. - **Union - `|`:** This operator creates a typeset that contains the members in the union of its operands. -- **Intersection - `|`:** This operator creates a typeset that contains the +- **Intersection - `&`:** This operator creates a typeset that contains the members in the intersection of its operands. -- **Subtraction - `\`:** This operator creates a typeset that contains all of - the members in the left operand that do not occur in the right operand. For information on the syntactic usage of these operators, please see the section on [type operators](#../syntax/types.md#type-operators) in the syntax