Add document the rule for the variant operator

informalsystems · Oct 6, 2023 · eed2ee6 · eed2ee6
1 parent 52baae9
commit eed2ee6
Showing 1 changed file with 9 additions and 0 deletions.
diff --git a/quint/src/types/specialConstraints.ts b/quint/src/types/specialConstraints.ts
@@ -181,6 +181,15 @@ export function itemConstraints(
   return right([constraint])
 }
 
+// The rule for the `variant` operator:
+//
+//   Γ ⊢ e: (t, c)            Γ ⊢ 'l' : str                v is fresh
+// --------------------------------------------------------------------
+//    Γ ⊢ variant('l', e) : (s, c /\ s ~ < l : t | v > /\ isDefined(s))
+//
+// Where < ... > is a row-based variant.
+//
+// This rule is explained in /doc/rfcs/rfc001-sum-types/rfc001-sum-types.org
 export function variantConstraints(
   id: bigint,
   args: [QuintEx, QuintType][],