Merge pull request #1581 from oliveredget/typo

Fix typos in docs

docs/codetour/.tours/coin.tour

@@ -22,7 +22,7 @@
     },
     {
       "title": "Declare pure functions",
-      "description": "\n\nIt often happens that a protocol requires auxilliary definitions that do not\ndepend on the protocol state, but only on the values of their parameters.\nSuch computations are often called \"pure\". In the above code, we define two\npure definitions:\n \n - The pure value `MAX_UINT`.\n\n - The pure definition `isUInt` that computes if a given integer `i` is within\n   the range from 0 to MAX_UINT (inclusive).\n\nThe main property of pure values is that they always return the same value.\nPure definitions always return the same value, if they are supplied with the\nsame arguments.\n\nTo see that no state is needed, evaluate these definitions in REPL\n(read-evaluate-print-loop):\n\n            \n>> echo \"MAX_UINT\" | quint -r ./lesson3-anatomy/coin.qnt::coin\n\n\n>> echo \"isUInt(22)\" | quint -r ./lesson3-anatomy/coin.qnt::coin\n\n\n>> echo \"isUInt(-1)\" | quint -r ./lesson3-anatomy/coin.qnt::coin\n\n\n>> echo \"isUInt(MAX_UINT + 1)\" | quint -r ./lesson3-anatomy/coin.qnt::coin\n\n\n\nThe functional layer is actually quite powerful; a lot of protocol behavior can\nbe defined here without referring to protocol state.\n\nAs you can see, we have omitted the type of `MAX_UINT` but specified the type of\n`isUInt`. Most of the time, the type checker can infer the types of values and\noperator definitions, and giving additional type annotations is up to you. In\nrare cases, the type checker may get confused, and then explicit type\nannotations will help you in figuring out the issue.\n            ",
+      "description": "\n\nIt often happens that a protocol requires auxiliary definitions that do not\ndepend on the protocol state, but only on the values of their parameters.\nSuch computations are often called \"pure\". In the above code, we define two\npure definitions:\n \n - The pure value `MAX_UINT`.\n\n - The pure definition `isUInt` that computes if a given integer `i` is within\n   the range from 0 to MAX_UINT (inclusive).\n\nThe main property of pure values is that they always return the same value.\nPure definitions always return the same value, if they are supplied with the\nsame arguments.\n\nTo see that no state is needed, evaluate these definitions in REPL\n(read-evaluate-print-loop):\n\n            \n>> echo \"MAX_UINT\" | quint -r ./lesson3-anatomy/coin.qnt::coin\n\n\n>> echo \"isUInt(22)\" | quint -r ./lesson3-anatomy/coin.qnt::coin\n\n\n>> echo \"isUInt(-1)\" | quint -r ./lesson3-anatomy/coin.qnt::coin\n\n\n>> echo \"isUInt(MAX_UINT + 1)\" | quint -r ./lesson3-anatomy/coin.qnt::coin\n\n\n\nThe functional layer is actually quite powerful; a lot of protocol behavior can\nbe defined here without referring to protocol state.\n\nAs you can see, we have omitted the type of `MAX_UINT` but specified the type of\n`isUInt`. Most of the time, the type checker can infer the types of values and\noperator definitions, and giving additional type annotations is up to you. In\nrare cases, the type checker may get confused, and then explicit type\nannotations will help you in figuring out the issue.\n            ",
       "line": 38,
       "file": "lesson3-anatomy/coin.qnt"
     },

docs/codetour/lesson0-helloworld/hello.template.qnt

@@ -181,7 +181,7 @@ Finally, the third statement may look useless to you too:
 Why shall we say that `readByUser` keeps its value in the next state?
 Most likely, we will be able to automatically infer this in the future.
 In the current version of Quint, if an action is used to execute transitions,
-it has to explicitely assign values to all of the state variables.
+it has to explicitly assign values to all of the state variables.
         </description>
       </step>
      !*/

docs/codetour/lesson0-helloworld/hello.xml

@@ -145,7 +145,7 @@ Finally, the third statement may look useless to you too:
 Why shall we say that `readByUser` keeps its value in the next state?
 Most likely, we will be able to automatically infer this in the future.
 In the current version of Quint, if an action is used to execute transitions,
-it has to explicitely assign values to all of the state variables.
+it has to explicitly assign values to all of the state variables.
         </description>
       </step>
       <step>

docs/codetour/lesson3-anatomy/coin.template.qnt

@@ -143,7 +143,7 @@ different kinds of "integers", when they are referred to via different type alia
         <title>Declare pure functions</title>
         <description>
 
-It often happens that a protocol requires auxilliary definitions that do not
+It often happens that a protocol requires auxiliary definitions that do not
 depend on the protocol state, but only on the values of their parameters.
 Such computations are often called "pure". In the above code, we define two
 pure definitions:

docs/codetour/lesson3-anatomy/coin.xml

@@ -98,7 +98,7 @@ different kinds of "integers", when they are referred to via different type alia
         <title>Declare pure functions</title>
         <description>
 
-It often happens that a protocol requires auxilliary definitions that do not
+It often happens that a protocol requires auxiliary definitions that do not
 depend on the protocol state, but only on the values of their parameters.
 Such computations are often called "pure". In the above code, we define two
 pure definitions:

docs/pages/docs/architecture-decision-records/adr008-managing-apalache.md

@@ -138,7 +138,7 @@ Pros:
 Cons:
 
 - Requires differing per-platform docs/instructions.
-- Requires maintaining per-platfrom packages; unclear who could provide and maintain these.
+- Requires maintaining per-platform packages; unclear who could provide and maintain these.
 - Quint is already available from npm.
 
 #### 3.2.2 Using an ecosystem package manager (npm, coursier, ...)
@@ -227,7 +227,7 @@ Cons:
 - Assumes that the JRE is installed on the local system.
 
 *Note: We did a prototype implementation querying the GitHub REST API in [#1115](https://github.com/informalsystems/quint/issues/1115).
-However, we observed CI issues due to the Github API's rate limiting as described in [#1124](https://github.com/informalsystems/quint/issues/1124). In pratice, the same issues can affect users (e.g., behind a shared IP) and may segnificantly impact UX of the `verify` command. As a countermeasure, we reverted to a hardcoded Apalache version in [`4ceb7d8`](https://github.com/informalsystems/quint/commit/4ceb7d8be824ddc0a2c2a14e105baff446f71e72).*
+However, we observed CI issues due to the Github API's rate limiting as described in [#1124](https://github.com/informalsystems/quint/issues/1124). In practice, the same issues can affect users (e.g., behind a shared IP) and may segnificantly impact UX of the `verify` command. As a countermeasure, we reverted to a hardcoded Apalache version in [`4ceb7d8`](https://github.com/informalsystems/quint/commit/4ceb7d8be824ddc0a2c2a14e105baff446f71e72).*
 
 #### 3.2.5 Apalache as cloud-hosted SaaS
 
@@ -237,7 +237,7 @@ is necessary.
 Pros:
 
 - No installation or server management issues.
-- Versioning and backwards-compatiblity could be exposed via separate endpoints.
+- Versioning and backwards-compatibility could be exposed via separate endpoints.
 
 Cons:
 
@@ -248,7 +248,7 @@ Cons:
 
 ### 3.3 Version dependencies between Quint and Apalache
 
-We want to maintain compatiblity between Quint and Apalache, therefore we need
+We want to maintain compatibility between Quint and Apalache, therefore we need
 some mode of linking compatible versions of both tools. Both tools follow
 [semantic versioning][].
 

docs/pages/docs/getting-started.mdx

@@ -16,7 +16,7 @@ npm i @informalsystems/quint -g
 
 ### Setup your code editor
 
-For the best experience writting Quint, you should set up your code editor with the Quint tools. The VSCode setup is, by far, the easiest, so you might want to use it if you want a quick start.
+For the best experience writing Quint, you should set up your code editor with the Quint tools. The VSCode setup is, by far, the easiest, so you might want to use it if you want a quick start.
 
 <Tabs items={['VSCode', 'Emacs', 'Vim']}>
  <Tabs.Tab>

docs/pages/docs/lessons/coin.md

@@ -130,7 +130,7 @@ different kinds of "integers", when they are referred to via different type alia
 
 
 
-It often happens that a protocol requires auxilliary definitions that do not
+It often happens that a protocol requires auxiliary definitions that do not
 depend on the protocol state, but only on the values of their parameters.
 Such computations are often called "pure". In the above code, we define two
 pure definitions:

docs/pages/docs/lessons/hello.md

@@ -182,7 +182,7 @@ Finally, the third statement may look useless to you too:
 Why shall we say that `readByUser` keeps its value in the next state?
 Most likely, we will be able to automatically infer this in the future.
 In the current version of Quint, if an action is used to execute transitions,
-it has to explicitely assign values to all of the state variables.
+it has to explicitly assign values to all of the state variables.
 
 ## 7. Introduce an action by the user
 

docs/theme.config.jsx

@@ -39,11 +39,11 @@ export default {
         <meta httpEquiv="Content-Language" content="en" />
         <meta
           name="description"
-          content="A modern and exectuable specification language"
+          content="A modern and executable specification language"
         />
         <meta
           name="og:description"
-          content="A modern and exectuable specification language"
+          content="A modern and executable specification language"
         />
         <meta name="twitter:card" content="summary_large_image" />
         <meta name="twitter:image" content="/og.png" />