Merge pull request #2970 from WalterSmuts/main

Typos: Run 'typos -w' command over docs/

docs/source/backends/javascript.rst

@@ -210,7 +210,7 @@ Handling JavaScript events
 
 
 In this example shows how to attach an event handler to a particular DOM element. Values of events
-are also associated with ``AnyPtr`` on the Idris side. To seperate ``DomNode`` form ``DomEvent``
+are also associated with ``AnyPtr`` on the Idris side. To separate ``DomNode`` form ``DomEvent``
 we create two different types. Also it demonstrates how a simple callback function defined in
 Idris can be used on the JavaScript side.
 

docs/source/backends/libraries.rst

@@ -22,7 +22,7 @@ for the idris name and name that appears in the compiled code, e.g.
     baz : Int
     baz = 42
 
-You can also specificy different names for different backends, in a similar way to %foreign
+You can also specify different names for different backends, in a similar way to %foreign
 
 .. code-block:: idris
 

docs/source/reference/builtins.rst

@@ -28,7 +28,7 @@ of another natural number. These are called Peano numbers.
 At runtime, Idris2 will automatically represent this the same as the ``Integer`` type.
 This will massively reduce the memory usage.
 
-There are a few rules governing when this optimization occures:
+There are a few rules governing when this optimization occurs:
 
 - The data type must have 2 constructors
 

docs/source/reference/packages.rst

@@ -191,7 +191,7 @@ and rely on a ``C`` support file. The FFI interface is documented elsewhere so w
 here. Once you do have a support file written in ``C``, you can build an ``so`` file using your
 package's post-build hook. Then, install (copy) that ``so`` file into the ``lib`` subfolder where
 Idris has installed your package in your post-install hook. When an executable depends on your package,
-Idris will copy shared object files from the ``lib`` directory into the build folder for the exectuable.
+Idris will copy shared object files from the ``lib`` directory into the build folder for the executable.
 
 Data files
 ----------

docs/source/reference/strings.rst

@@ -72,7 +72,7 @@ literals the characters ``\\`` and ``"`` must be escaped, for multiline strings
 escaped
 sequence in order to avoid having to escape those very common sets of characters. For this, use
 ``#"`` as starting delimiter and ``"#`` as closing delimiter. The number of ``#`` symbols can be
-increased in order to accomodate for edge cases where ``"#`` would be a valid symbol.
+increased in order to accommodate for edge cases where ``"#`` would be a valid symbol.
 In the following example we are able to match on ``\{`` by using half as many ``\\`` characters
 as if we didn't use raw string literals:
 

docs/source/tutorial/typesfuns.rst

@@ -628,7 +628,7 @@ the run-time system. We’ve already seen one I/O program:
 
 The type of ``putStrLn`` explains that it takes a string, and returns
 an I/O action which produces an element of the unit type ``()``. There is a
-variant ``putStr`` which decribes the output of a string without a newline:
+variant ``putStr`` which describes the output of a string without a newline:
 
 .. code-block:: idris
 

docs/source/typedd/typedd.rst

@@ -78,7 +78,7 @@ Chapter 5
 ---------
 
 Although there is a ``Cast`` instance from ``String`` to ``Nat``, its
-behaviour of returing Z if the ``String`` is not numeric is now thought to be
+behaviour of returning Z if the ``String`` is not numeric is now thought to be
 confusing and potentially error prone. Instead, there is ``stringToNatOrZ`` in
 ``Data.String`` which at least has a clearer name. So:
 

docs/source/updates/updates.rst

@@ -311,7 +311,7 @@ So if you have the following, all in the same file...
 
       export
       aVisible : Int -> Int
-      aVisibile x = aHidden x
+      aVisible x = aHidden x
 
     namespace B
       export

libs/papers/Language/IntrinsicScoping/TypeTheory.idr

@@ -63,9 +63,9 @@ data Infer : Scoped where
   -- This is fairly unconventional: in order to support overloaded
   -- data constructors disambiguated in a type-direct manner, we would
   -- typically put zero, suc, & friends in `Check`.
-  ||| The zero constructor is inferable
+  ||| The zero constructor is inferrable
   Zro : Infer f g
-  ||| The successor constructor is inferable
+  ||| The successor constructor is inferrable
   Suc : Check f g -> Infer f g
   ||| Pi is inferrable
   Pi : (a : Check f g) -> (b : Abs Check f g) -> Infer f g
@@ -82,7 +82,7 @@ infixl 3 `App`
 
 total
 data Check : Scoped where
-  ||| Inferable terms are trivially checkable
+  ||| Inferrable terms are trivially checkable
   Emb : Infer f g -> Check f g
   ||| A function binding its argument
   Lam : Abs Check f g -> Check f g

libs/papers/Language/TypeTheory.idr

@@ -74,7 +74,7 @@ namespace Section2
 
   -- Raw terms are neither scopechecked nor typecked
 
-  ||| Inferable terms know what their type is
+  ||| Inferrable terms know what their type is
   data Infer : Type
 
   ||| Checkable terms need to be checked against a type
@@ -97,7 +97,7 @@ namespace Section2
 
   total
   data Check : Type where
-    ||| Inferable terms are trivially checkable
+    ||| Inferrable terms are trivially checkable
     Emb : Infer -> Check
     ||| A function binding its argument
     Lam : Abs Check -> Check
@@ -365,7 +365,7 @@ namespace Section3
 
   total
   data Check : Type where
-    ||| Inferable terms are trivially checkable
+    ||| Inferrable terms are trivially checkable
     Emb : Infer -> Check
     ||| A function binding its argument
     Lam : Abs Check -> Check
@@ -587,9 +587,9 @@ namespace Section4
     --   ps : Abs (Abs Check)
     --   n : Check
     Rec : (pred, pz, ps : Check) -> (n : Check) -> Infer
-    ||| The zero constructor is inferable
+    ||| The zero constructor is inferrable
     Zro : Infer
-    ||| The successor constructor is inferable
+    ||| The successor constructor is inferrable
     Suc : Check -> Infer
     ||| Pi is inferrable
     Pi : (a : Check) -> (b : Abs Check) -> Infer
@@ -606,7 +606,7 @@ namespace Section4
 
   total
   data Check : Type where
-    ||| Inferable terms are trivially checkable
+    ||| Inferrable terms are trivially checkable
     Emb : Infer -> Check
     ||| A function binding its argument
     Lam : Abs Check -> Check