chore: fix some typos

docs/content/docs/quint.md

@@ -264,7 +264,7 @@ Options:
  found during the execution. When the parameter `--out` is supplied, the trace
  is written as a JSON representation of Quint IR in the output file. When the
  parameter `--out-itf` is supplied, the traces are written in the [Informal Trace
- Format][]. This output can be conviently displayed with the [ITF Trace
+ Format][]. This output can be conveniently displayed with the [ITF Trace
  Viewer][], or just with [jq][].
 
  - If the specification cannot be run (e.g., due to a parsing error), the file
@@ -402,7 +402,7 @@ Viewer][], or just with [jq][].
 
 - When a `--inductive-invariant` is supplied, Quint will call Apalache multiple times:
   - 2 times if there is no ordinary invariant (`--invariant`)
-    - First, checking that the inductive invariant holds in all intiial states
+    - First, checking that the inductive invariant holds in all initial states
       - `init=init`, `invariant=inductive-invariant`, `max-steps=0`
     - Then, checking that, starting from a state where inductive invariant
       holds, if we take a step, the inductive invariant will continue to hold.

evaluator/fixtures/jmt/apply_simple.qnt

@@ -113,7 +113,7 @@ module apply_simple {
     // We will construct the three from the leafs up until the root
     // Say we want to construct a tree with nodes: 0000, 0001, 1111
     // We start from MAX_HASH_LENGTH - 1, which is 3 (i = 3)
-    // We then find all prefixes of lenght 3 in the current nodes: 000 and 111
+    // We then find all prefixes of length 3 in the current nodes: 000 and 111
     // For each prefix, we do something.
     // For prefix 000: try to find both 000.append(0) and 000.append(1) in the current nodes
     //   - If both exist, then push 000 as an internal node both of them as children to the queue