chore: fix spelling mistakes in examples (doc/examples/) (#5434)

Co-authored-by: euprunin <euprunin@users.noreply.github.com>

doc/examples/ICERM2022/ctor.lean

@@ -18,7 +18,7 @@ def ctor (mvarId : MVarId) (idx : Nat) : MetaM (List MVarId) := do
     else if h : idx - 1 < ctors.length then
       mvarId.apply (.const ctors[idx - 1] us)
     else
-      throwTacticEx `ctor mvarId "invalid index, inductive datatype has only {ctors.length} contructors"
+      throwTacticEx `ctor mvarId "invalid index, inductive datatype has only {ctors.length} constructors"
 
 open Elab Tactic
 

doc/examples/deBruijn.lean

@@ -149,7 +149,7 @@ We now define the constant folding optimization that traverses a term if replace
 /-!
 The correctness of the `Term.constFold` is proved using induction, case-analysis, and the term simplifier.
 We prove all cases but the one for `plus` using `simp [*]`. This tactic instructs the term simplifier to
-use hypotheses such as `a = b` as rewriting/simplications rules.
+use hypotheses such as `a = b` as rewriting/simplifications rules.
 We use the `split` to break the nested `match` expression in the `plus` case into two cases.
 The local variables `iha` and `ihb` are the induction hypotheses for `a` and `b`.
 The modifier `←` in a term simplifier argument instructs the term simplifier to use the equation as a rewriting rule in

doc/examples/phoas.lean

@@ -225,7 +225,7 @@ We now define the constant folding optimization that traverses a term if replace
 /-!
 The correctness of the `constFold` is proved using induction, case-analysis, and the term simplifier.
 We prove all cases but the one for `plus` using `simp [*]`. This tactic instructs the term simplifier to
-use hypotheses such as `a = b` as rewriting/simplications rules.
+use hypotheses such as `a = b` as rewriting/simplifications rules.
 We use the `split` to break the nested `match` expression in the `plus` case into two cases.
 The local variables `iha` and `ihb` are the induction hypotheses for `a` and `b`.
 The modifier `←` in a term simplifier argument instructs the term simplifier to use the equation as a rewriting rule in

doc/examples/widgets.lean

@@ -93,7 +93,7 @@ Meaning "Remote Procedure Call",this is a Lean function callable from widget cod
 Our method will take in the `name : Name` of a constant in the environment and return its type.
 By convention, we represent the input data as a `structure`.
 Since it will be sent over from JavaScript,
-we need `FromJson` and `ToJson` instnace.
+we need `FromJson` and `ToJson` instance.
 We'll see why the position field is needed later.
 -/