From c5d29aa9d1d298d445024da84ee7986e94ee1bb1 Mon Sep 17 00:00:00 2001 From: Yazalde Filimone Date: Fri, 14 Nov 2025 17:15:34 +0200 Subject: [PATCH 01/10] refactor: replace lodash.isequal with node:util.isDeepStrictEqual, #1606 --- CONTRIBUTING.md | 42 ++++++++++++++++---------------- quint/package-lock.json | 6 ----- quint/package.json | 1 - quint/src/effects/base.ts | 2 +- quint/src/effects/modeChecker.ts | 2 +- quint/src/util.ts | 9 +++++++ 6 files changed, 32 insertions(+), 30 deletions(-) diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md index 51e1c69e3..643ba2ccb 100644 --- a/CONTRIBUTING.md +++ b/CONTRIBUTING.md @@ -1,6 +1,6 @@ # Contributing -Welcome to the Quint repository! We are excited that you want to contribute to +Welcome to the Quint repository! We are excited that you want to contribute to Quint, whether it is by reporting issues, suggesting features, or writing code. ## Table of Contents @@ -78,7 +78,7 @@ This repository hosts all Quint pieces: - [ADR002: Error codes](./docs/content/docs/development-docs/architecture-decision-records/adr002-errors.md) - [ADR003: Interface to visit Internal Representation - components](./docs/content/docs/development-docs/architecture-decision-records/adr003-visiting-ir-components.md) + components](./docs/content/docs/development-docs/architecture-decision-records/adr003-visiting-ir-components.md) - [ADR004: An Effect System for Quint](./docs/content/docs/development-docs/architecture-decision-records/adr004-effect-system.md) - [ADR005: A Type System for @@ -280,14 +280,14 @@ ln -s $PWD/vscode/quint-vscode/ $HOME/.vscode/extensions/informal.quint-vscode-X We use `yalc` to manage unpublished packages. To install it, run -``` sh +```sh npm i yalc -g ``` Then use the `local` make target to replace the published version of `quint` with the local one and build the extension: -``` sh +```sh make local ``` @@ -308,13 +308,13 @@ Write unit tests in [quint/test](./quint/test), add test data to [quint/testFixture](./quint/testFixture). To run the tests and check code coverage, run the following commands (in the [quint](./quint) folder): - 1. Run unit tests: +1. Run unit tests: ```sh npm run test ``` - 1. Check code coverage with tests: +1. Check code coverage with tests: ```sh npm run coverage @@ -326,7 +326,7 @@ When adding a new test fixture or updating an existing one, you might need to generate the `.json` and `.map.json` files used in test expectations. For that, run: -``` sh +```sh npm run update-fixtures ``` @@ -365,10 +365,10 @@ The files containing tests for `txm` are: Run integration tests: - ```sh - npm run compile && npm link && npm run integration - ``` - +```sh +npm run compile && npm link && npm run integration +``` + PS: this will not run the Apalache-related tests, as they usually won't break as consequences of changes in the Quint codebase. They are run in the CI, and you can run them locally by running `npm run apalache-integration` and `npm run @@ -388,7 +388,7 @@ To [add a new dependency for integration tests or other development purposes](https://docs.npmjs.com/specifying-dependencies-and-devdependencies-in-a-package-json-file) run: -``` sh +```sh npm install --save-dev ``` @@ -402,7 +402,7 @@ To [add a new dependency for integration tests or other development purposes](https://doc.rust-lang.org/cargo/reference/specifying-dependencies.html) run: -``` sh +```sh cargo add --dev ``` @@ -436,7 +436,7 @@ lose the advantage of exhaustiveness checking. Here's an example: Assume we have a type `T` ```typescript -type T = 'a' | 'b' | 'c' +type T = "a" | "b" | "c"; ``` We should structure our program such that @@ -445,7 +445,7 @@ We should structure our program such that - whenever a new alternative is added to this type, the type system will warn us about all the places we need to account for the new kind of data. -If we use `T` with a `switch` or `if`/`then` statement that *returns values*, +If we use `T` with a `switch` or `if`/`then` statement that _returns values_, this indispensable help is ensured. E.g., if we try to write the following: ```typescript @@ -535,12 +535,12 @@ false false ``` -For this reason, we are using `isEqual` provided by the [lodash.isequal][] +For this reason, we are using `isEqual` provided by the [node:util][] package: ```js > import { none, just } from '@sweet-monads/maybe' -> import isEqual from 'lodash.isequal' +> import { isEqual } from '../util' > isEqual(just(true), just(true)) true > isEqual(none(), none()) @@ -569,12 +569,12 @@ type that can be used to represent a value that can either be a success or a failure. ```typescript -import { left, right } from '@sweet-monads/either' +import { left, right } from "@sweet-monads/either"; if (all_good(expr)) { - return right(value) + return right(value); } else { - return left({ code: 'QNT500', message: `${expr} is not good!`, reference: expr.id }) + return left({ code: "QNT500", message: `${expr} is not good!`, reference: expr.id }); } ``` @@ -606,7 +606,7 @@ the Rust evaluator and the VSCode extension + the language server. This will trigger the release and publication of the package to npm and GitHub. - + ### Evaluator The evaluator is the latest addition to the Quint repository, and it's release diff --git a/quint/package-lock.json b/quint/package-lock.json index ae5c63e6e..3bc283b2e 100644 --- a/quint/package-lock.json +++ b/quint/package-lock.json @@ -28,7 +28,6 @@ "line-column": "^1.0.2", "lodash": "^4.17.21", "lodash.clonedeep": "4.5.0", - "lodash.isequal": "^4.5.0", "seedrandom": "^3.0.5", "tar": "^6.1.14", "yargs": "^17.7.2" @@ -6588,11 +6587,6 @@ "integrity": "sha512-uHaJFihxmJcEX3kT4I23ABqKKalJ/zDrDg0lsFtc1h+3uw49SIJ5beyhx5ExVRti3AvKoOJngIj7xz3oylPdWQ==", "dev": true }, - "node_modules/lodash.isequal": { - "version": "4.5.0", - "resolved": "https://registry.npmjs.org/lodash.isequal/-/lodash.isequal-4.5.0.tgz", - "integrity": "sha512-pDo3lu8Jhfjqls6GkMgpahsF9kCyayhgykjyLMNFTKWrpVdAQtYyB4muAMWozBB4ig/dtWAmsMxLEI8wuz+DYQ==" - }, "node_modules/lodash.merge": { "version": "4.6.2", "resolved": "https://registry.npmjs.org/lodash.merge/-/lodash.merge-4.6.2.tgz", diff --git a/quint/package.json b/quint/package.json index bb8b382ad..f51648ddd 100644 --- a/quint/package.json +++ b/quint/package.json @@ -67,7 +67,6 @@ "line-column": "^1.0.2", "lodash": "^4.17.21", "lodash.clonedeep": "4.5.0", - "lodash.isequal": "^4.5.0", "seedrandom": "^3.0.5", "tar": "^6.1.14", "yargs": "^17.7.2" diff --git a/quint/src/effects/base.ts b/quint/src/effects/base.ts index f2419c052..3e5821d37 100644 --- a/quint/src/effects/base.ts +++ b/quint/src/effects/base.ts @@ -17,7 +17,7 @@ import { Either, left, mergeInMany, right } from '@sweet-monads/either' import { Substitutions, applySubstitution, applySubstitutionToEntity, compose } from './substitutions' import { Error, ErrorTree, buildErrorLeaf, buildErrorTree } from '../errorTree' import { flattenUnions, simplify } from './simplification' -import isEqual from 'lodash.isequal' +import { isEqual } from '../util' import { differenceWith, intersectionWith } from 'lodash' /* Kinds for concrete effect components */ diff --git a/quint/src/effects/modeChecker.ts b/quint/src/effects/modeChecker.ts index 8a657cc2b..e1019ed26 100644 --- a/quint/src/effects/modeChecker.ts +++ b/quint/src/effects/modeChecker.ts @@ -13,7 +13,7 @@ * @module */ -import isEqual from 'lodash.isequal' +import { isEqual } from '../util' import { qualifierToString } from '../ir/IRprinting' import { IRVisitor, walkDeclaration } from '../ir/IRVisitor' import { QuintError } from '../quintError' diff --git a/quint/src/util.ts b/quint/src/util.ts index 2ce0caf95..714510082 100644 --- a/quint/src/util.ts +++ b/quint/src/util.ts @@ -15,6 +15,7 @@ import JSONbig from 'json-bigint' import lodash from 'lodash' import { Maybe, none } from '@sweet-monads/maybe' +import { isDeepStrictEqual } from 'node:util' /** Add this at the end of a switch statement or if/then sequence to enforce exhaustiveness checking * @@ -112,3 +113,11 @@ function findInsertionIndex(array: A[], pred: (a: A) => boolean): number { return low } + +/** + * This function replaces `lodash.isEqual` using the native Node.js implementation. + * + */ +export function isEqual(left: L, right: R): boolean { + return isDeepStrictEqual(left, right) +} From 79b85f3e8a9700d2644059adeb0364f881cf7ae0 Mon Sep 17 00:00:00 2001 From: Yazalde Filimone Date: Sat, 15 Nov 2025 23:32:59 +0200 Subject: [PATCH 02/10] refactor: replace lodash.isequal with node:util.isDeepStrictEqual, #1606 --- quint/src/effects/simplification.ts | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/quint/src/effects/simplification.ts b/quint/src/effects/simplification.ts index ec4b65501..aa574917c 100644 --- a/quint/src/effects/simplification.ts +++ b/quint/src/effects/simplification.ts @@ -12,8 +12,7 @@ * @module */ -import isEqual from 'lodash.isequal' -import { unreachable } from '../util' +import { isEqual, unreachable } from '../util' import { ConcreteEffect, Effect, Entity, StateVariable } from './base' /** From 31e9fbb5112e01d69772e5728c3f74e5284f0ede Mon Sep 17 00:00:00 2001 From: Yazalde Filimone Date: Fri, 28 Nov 2025 23:26:18 +0200 Subject: [PATCH 03/10] Update CONTRIBUTING.md Co-authored-by: Gabriela Moreira --- CONTRIBUTING.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md index 643ba2ccb..728fb4c2c 100644 --- a/CONTRIBUTING.md +++ b/CONTRIBUTING.md @@ -572,7 +572,7 @@ failure. import { left, right } from "@sweet-monads/either"; if (all_good(expr)) { - return right(value); + return right(value) } else { return left({ code: "QNT500", message: `${expr} is not good!`, reference: expr.id }); } From e7079399b87b9d52b7e90ac86b6afcfe680a830b Mon Sep 17 00:00:00 2001 From: Yazalde Filimone Date: Fri, 28 Nov 2025 23:26:29 +0200 Subject: [PATCH 04/10] Update CONTRIBUTING.md Co-authored-by: Gabriela Moreira --- CONTRIBUTING.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md index 728fb4c2c..73252a449 100644 --- a/CONTRIBUTING.md +++ b/CONTRIBUTING.md @@ -569,7 +569,7 @@ type that can be used to represent a value that can either be a success or a failure. ```typescript -import { left, right } from "@sweet-monads/either"; +import { left, right } from '@sweet-monads/either' if (all_good(expr)) { return right(value) From 3332cc952cf561e79dfc7b1176d319809901aa47 Mon Sep 17 00:00:00 2001 From: Yazalde Filimone Date: Fri, 28 Nov 2025 23:26:37 +0200 Subject: [PATCH 05/10] Update CONTRIBUTING.md Co-authored-by: Gabriela Moreira --- CONTRIBUTING.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md index 73252a449..2f739ce9c 100644 --- a/CONTRIBUTING.md +++ b/CONTRIBUTING.md @@ -436,7 +436,7 @@ lose the advantage of exhaustiveness checking. Here's an example: Assume we have a type `T` ```typescript -type T = "a" | "b" | "c"; +type T = 'a' | 'b' | 'c'; ``` We should structure our program such that From e7a05e786710fd785d60ddd052cfc6a500b72c40 Mon Sep 17 00:00:00 2001 From: Yazalde Filimone Date: Fri, 28 Nov 2025 23:26:45 +0200 Subject: [PATCH 06/10] Update CONTRIBUTING.md Co-authored-by: Gabriela Moreira --- CONTRIBUTING.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md index 2f739ce9c..ab09a06fe 100644 --- a/CONTRIBUTING.md +++ b/CONTRIBUTING.md @@ -574,7 +574,7 @@ import { left, right } from '@sweet-monads/either' if (all_good(expr)) { return right(value) } else { - return left({ code: "QNT500", message: `${expr} is not good!`, reference: expr.id }); + return left({ code: 'QNT500', message: `${expr} is not good!`, reference: expr.id }) } ``` From 970ccffab0df3f0f7cb5b72241b369345871a56f Mon Sep 17 00:00:00 2001 From: Yazalde Filimone Date: Fri, 28 Nov 2025 23:38:18 +0200 Subject: [PATCH 07/10] refactor: remove function --- quint/src/effects/base.ts | 12 ++++++------ quint/src/effects/modeChecker.ts | 6 +++--- quint/src/effects/simplification.ts | 2 +- quint/src/effects/substitutions.ts | 2 +- quint/src/runtime/impl/nondet.ts | 2 +- quint/src/types/substitutions.ts | 2 +- quint/src/util.ts | 2 +- 7 files changed, 14 insertions(+), 14 deletions(-) diff --git a/quint/src/effects/base.ts b/quint/src/effects/base.ts index 3e5821d37..a646805ef 100644 --- a/quint/src/effects/base.ts +++ b/quint/src/effects/base.ts @@ -17,7 +17,7 @@ import { Either, left, mergeInMany, right } from '@sweet-monads/either' import { Substitutions, applySubstitution, applySubstitutionToEntity, compose } from './substitutions' import { Error, ErrorTree, buildErrorLeaf, buildErrorTree } from '../errorTree' import { flattenUnions, simplify } from './simplification' -import { isEqual } from '../util' +import { isDeepStrictEqual } from 'node:util' import { differenceWith, intersectionWith } from 'lodash' /* Kinds for concrete effect components */ @@ -332,7 +332,7 @@ export function unifyEntities(va: Entity, vb: Entity): Either v.name)), new Set(v2.stateVariables.map(v => v.name)))) { + if (isDeepStrictEqual(new Set(v1.stateVariables.map(v => v.name)), new Set(v2.stateVariables.map(v => v.name)))) { return right([]) } else { return left({ @@ -349,7 +349,7 @@ export function unifyEntities(va: Entity, vb: Entity): Either unifyEntities(v, v2))) @@ -358,10 +358,10 @@ export function unifyEntities(va: Entity, vb: Entity): Either 0) { - const s1 = { ...v1, entities: differenceWith(v1.entities, intersection, isEqual) } - const s2 = { ...v2, entities: differenceWith(v2.entities, intersection, isEqual) } + const s1 = { ...v1, entities: differenceWith(v1.entities, intersection, isDeepStrictEqual) } + const s2 = { ...v2, entities: differenceWith(v2.entities, intersection, isDeepStrictEqual) } // There was an intersection, try to unify the remaining entities return unifyEntities(s1, s2) diff --git a/quint/src/effects/modeChecker.ts b/quint/src/effects/modeChecker.ts index e1019ed26..8b29593f7 100644 --- a/quint/src/effects/modeChecker.ts +++ b/quint/src/effects/modeChecker.ts @@ -13,7 +13,7 @@ * @module */ -import { isEqual } from '../util' +import { isDeepStrictEqual } from 'node:util' import { qualifierToString } from '../ir/IRprinting' import { IRVisitor, walkDeclaration } from '../ir/IRVisitor' import { QuintError } from '../quintError' @@ -248,7 +248,7 @@ function addedEntities(paramEntities: Entity[], resultEntity: Entity): Entity[] case 'union': return resultEntity.entities.flatMap(entity => addedEntities(paramEntities, entity)) case 'concrete': { - const vars = resultEntity.stateVariables.filter(v => !paramEntities.some(p => isEqual(p, v))) + const vars = resultEntity.stateVariables.filter(v => !paramEntities.some(p => isDeepStrictEqual(p, v))) if (vars.length === 0) { return [] } @@ -256,7 +256,7 @@ function addedEntities(paramEntities: Entity[], resultEntity: Entity): Entity[] return [{ kind: 'concrete', stateVariables: vars }] } case 'variable': - return !paramEntities.some(p => isEqual(p, resultEntity)) ? [resultEntity] : [] + return !paramEntities.some(p => isDeepStrictEqual(p, resultEntity)) ? [resultEntity] : [] } } diff --git a/quint/src/effects/simplification.ts b/quint/src/effects/simplification.ts index aa574917c..0d2b76ea2 100644 --- a/quint/src/effects/simplification.ts +++ b/quint/src/effects/simplification.ts @@ -99,7 +99,7 @@ function deduplicateEntity(entity: Entity): Entity { const nestedEntities = entity.entities.map(v => deduplicateEntity(v)) const unique: Entity[] = [] nestedEntities.forEach(entity => { - if (!unique.some(v => isEqual(v, entity))) { + if (!unique.some(v => isDeepStrictEqual(v, entity))) { unique.push(entity) } }) diff --git a/quint/src/effects/substitutions.ts b/quint/src/effects/substitutions.ts index 0ab10600a..19b2885f8 100644 --- a/quint/src/effects/substitutions.ts +++ b/quint/src/effects/substitutions.ts @@ -88,7 +88,7 @@ export function applySubstitution(subs: Substitutions, e: Effect): Either { - if (!isEqual(r, e)) { + if (!isDeepStrictEqual(r, e)) { // Keep re-applying the substitutions until the effect is unchanged. // Useful when substitutions have a transitive pattern [ a |-> b, b |-> c ] return applySubstitution(subs, r) diff --git a/quint/src/runtime/impl/nondet.ts b/quint/src/runtime/impl/nondet.ts index 93d36e6bb..b711e7d23 100644 --- a/quint/src/runtime/impl/nondet.ts +++ b/quint/src/runtime/impl/nondet.ts @@ -92,7 +92,7 @@ export function evalNondet( } // Retry if condition is satisfied and we haven't exhausted all possible positions. - } while (shouldRetry && !isEqual(newPositions, originalPositions)) + } while (shouldRetry && !isDeepStrictEqual(newPositions, originalPositions)) // Reset the cache cache.value = undefined diff --git a/quint/src/types/substitutions.ts b/quint/src/types/substitutions.ts index 3cec9d93c..e116e5f5d 100644 --- a/quint/src/types/substitutions.ts +++ b/quint/src/types/substitutions.ts @@ -113,7 +113,7 @@ export function applySubstitution(table: LookupTable, subs: Substitutions, t: Qu } const result = singleApplication() - if (isEqual(result, t)) { + if (isDeepStrictEqual(result, t)) { return t } else { return applySubstitution(table, subs, result) diff --git a/quint/src/util.ts b/quint/src/util.ts index 714510082..c15e00085 100644 --- a/quint/src/util.ts +++ b/quint/src/util.ts @@ -57,7 +57,7 @@ export function zip(a: A[], b: B[]): [A, B][] { * * ``` * const result = findMap([1,2,3], (x) => x % 2 === 0 ? just(x) : none()) - * lodash.isEqual(result, just(2)) + * lodash.isDeepStrictEqual(result, just(2)) * ``` * */ export function findMap(xs: Iterable, f: (x: X) => Maybe): Maybe { From f875303cb15ada2ff6703effdfb1e4a1980f441d Mon Sep 17 00:00:00 2001 From: Yazalde Filimone Date: Fri, 28 Nov 2025 23:53:48 +0200 Subject: [PATCH 08/10] update contributing.md --- CONTRIBUTING.md | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md index ab09a06fe..c9fc71ebd 100644 --- a/CONTRIBUTING.md +++ b/CONTRIBUTING.md @@ -540,10 +540,10 @@ package: ```js > import { none, just } from '@sweet-monads/maybe' -> import { isEqual } from '../util' -> isEqual(just(true), just(true)) +> import { isDeepStrictEqual } from 'node:util' +> isDeepStrictEqual(just(true), just(true)) true -> isEqual(none(), none()) +> isDeepStrictEqual(none(), none()) true ``` From 53f5d6f6716901e36a60a6b4b9d700c2d04e43f6 Mon Sep 17 00:00:00 2001 From: Yazalde Filimone Date: Fri, 12 Dec 2025 15:47:30 +0200 Subject: [PATCH 09/10] refactor: remove function --- quint/src/util.ts | 9 --------- 1 file changed, 9 deletions(-) diff --git a/quint/src/util.ts b/quint/src/util.ts index c15e00085..153b7631a 100644 --- a/quint/src/util.ts +++ b/quint/src/util.ts @@ -15,7 +15,6 @@ import JSONbig from 'json-bigint' import lodash from 'lodash' import { Maybe, none } from '@sweet-monads/maybe' -import { isDeepStrictEqual } from 'node:util' /** Add this at the end of a switch statement or if/then sequence to enforce exhaustiveness checking * @@ -113,11 +112,3 @@ function findInsertionIndex(array: A[], pred: (a: A) => boolean): number { return low } - -/** - * This function replaces `lodash.isEqual` using the native Node.js implementation. - * - */ -export function isEqual(left: L, right: R): boolean { - return isDeepStrictEqual(left, right) -} From 1ed7da8bf3552adf975857d52c5be6e5eabc2fe5 Mon Sep 17 00:00:00 2001 From: Yazalde Filimone Date: Tue, 16 Dec 2025 17:37:27 +0200 Subject: [PATCH 10/10] refactor: replace isEqual to isDeepStrictEqual and resolve missing import, #1606 --- quint/src/effects/simplification.ts | 3 ++- quint/src/effects/substitutions.ts | 2 +- quint/src/runtime/impl/nondet.ts | 2 +- quint/src/types/substitutions.ts | 2 +- 4 files changed, 5 insertions(+), 4 deletions(-) diff --git a/quint/src/effects/simplification.ts b/quint/src/effects/simplification.ts index 0d2b76ea2..900364af7 100644 --- a/quint/src/effects/simplification.ts +++ b/quint/src/effects/simplification.ts @@ -12,8 +12,9 @@ * @module */ -import { isEqual, unreachable } from '../util' +import { unreachable } from '../util' import { ConcreteEffect, Effect, Entity, StateVariable } from './base' +import { isDeepStrictEqual } from 'node:util' /** * Simplifies a concrete effect by: diff --git a/quint/src/effects/substitutions.ts b/quint/src/effects/substitutions.ts index 282134fd8..0f1e63959 100644 --- a/quint/src/effects/substitutions.ts +++ b/quint/src/effects/substitutions.ts @@ -17,7 +17,7 @@ import { ErrorTree, buildErrorTree } from '../errorTree' import { Effect, Entity } from './base' import { effectToString, substitutionsToString } from './printing' import { simplify } from './simplification' -import { isEqual } from 'lodash' +import { isDeepStrictEqual } from 'node:util' /* * Substitutions can be applied to both effects and entities, replacing diff --git a/quint/src/runtime/impl/nondet.ts b/quint/src/runtime/impl/nondet.ts index b711e7d23..9195c6df7 100644 --- a/quint/src/runtime/impl/nondet.ts +++ b/quint/src/runtime/impl/nondet.ts @@ -15,7 +15,7 @@ import { Either, right } from '@sweet-monads/either' import { EvalFunction } from './builder' import { RuntimeValue, rv } from './runtimeValue' -import { isEqual } from 'lodash' +import { isDeepStrictEqual } from 'node:util' import { QuintError } from '../../quintError' import { CachedValue } from './Context' import { Maybe } from '@sweet-monads/maybe' diff --git a/quint/src/types/substitutions.ts b/quint/src/types/substitutions.ts index 1315a5152..0713a0ba2 100644 --- a/quint/src/types/substitutions.ts +++ b/quint/src/types/substitutions.ts @@ -19,7 +19,7 @@ import { ConcreteFixedRow, QuintType, Row } from '../ir/quintTypes' import { Constraint } from './base' import { unify, unifyRows } from './constraintSolver' import { substitutionsToString } from './printing' -import { isEqual } from 'lodash' +import { isDeepStrictEqual } from 'node:util' /* * Substitutions can be applied to Quint types, type variables with another type