# Quint Authors - Language Basics (Highlights)  ## Metadata **Review**:: [readwise.io](https://readwise.io/bookreview/57479565) **Source**:: #from/readwise #from/reader **Zettel**:: #zettel/fleeting **Status**:: #x **Authors**:: [[Quint Authors]] **Full Title**:: Language Basics **Category**:: #articles #readwise/articles **Category Icon**:: 📰 **URL**:: [quint-lang.org](https://quint-lang.org/docs/language-basics) **Host**:: [[quint-lang.org]] **Highlighted**:: [[2026-01-10]] **Created**:: [[2026-01-10]] ## Highlights - Although in theory (and in TLA+) you could apply the prime operator to any expression, in Quint it has to always come in the format `<var>' = <expr>` which is called assignment. This prevents us from writing things that are really hard to grasp and potentially not possible to compute with the available tools. ([View Highlight](https://read.readwise.io/read/01kek3fmdgkm07d1g7d57q039w)) ^976020103 - Quint’s tooling is equipped to report several different errors if you use `'` in forbidden ways. It won’t let you assign a value to a variable more than once in the same transition, or forget to update a variable in some branches of transitions. ([View Highlight](https://read.readwise.io/read/01kek3g8h309s3e4cygy9map6j)) ^976020118 - Actions named `init` and `step` are special as they define the **state machine**. Action `init` defines the initial states and `step` defines the transitions (you can use different names and specify the on the CLI, but `init` and `step` are the defaults). ([View Highlight](https://read.readwise.io/read/01kek3htrwxr7t0yzp01w34tqf)) ^976020154 - In Quint models, we express all of these possibilities using `any` and `oneOf`. ([View Highlight](https://read.readwise.io/read/01kek3mmx2a60pfpthrwv8wszf)) ^976020344 - Definitions prefixed with `pure` are just like functional programming functions: given the same input (parameters), they will always return the same output. ([View Highlight](https://read.readwise.io/read/01kek3nmrjxzddrsj934a0b3my)) ^976020367 - Definitions that don’t take parameters can be of mode `val` (or `pure val`), while definitions that take parameters need to be `def` (or `pure def`). ([View Highlight](https://read.readwise.io/read/01kek3pk224tpcmcvz8nqwktys)) ^976020380 - Definitions that use the prime operator (`'`) can only be of mode `action`. Actions are definitions that “modify” the state. ([View Highlight](https://read.readwise.io/read/01kek3q566ynw6fs9fnzb849s9)) ^976020389 - Non-deterministic definitions are special ones: you can use them only inside actions, before some assignment(s), in order to pick a value non-deterministically. ([View Highlight](https://read.readwise.io/read/01kek3qkrej6vf8tqf5tg4sefp)) ^976020417 - Quint doesn’t support recursive operators, mutually recursive operators, nor recursive type definitions. ([View Highlight](https://read.readwise.io/read/01kek3rjp4rfsnwytbhfccvbnw)) ^976020426 - all recursion that it could, in theory, support, is the type of recursion that can be written using folds ([View Highlight](https://read.readwise.io/read/01kek3t3ev3fxe4wb3wkjdsjae)) ^976020471