Fixed a few typos

ARCHITECTURE.md

@@ -19,7 +19,7 @@ Contains the frontend to Rules and Patterns (`@rule` macro and `Pattern` functio
 # EGraphs Module 
 Contains code for the e-graphs rewriting backend. See [egg paper](https://dl.acm.org/doi/pdf/10.1145/3434304) for an high level overview.
 
-- `egraphs.jl`: Definition of `ENode`, `EClass` and `EGraph` types, EClass unioning, metadata access, defintion of EGraphs, adding, merging, rebuilding.
+- `egraphs.jl`: Definition of `ENode`, `EClass` and `EGraph` types, EClass unioning, metadata access, definition of EGraphs, adding, merging, rebuilding.
 - `ematch.jl`: E-Graph Pattern matching virtual machine interpreter.
 - `analysis.jl`: Core algorithms for analyzing egraphs and extracting terms from egraphs.
 - `saturation.jl`: Core algorithm for equality saturation, rewriting on e-graphs, e-graphs search.  Search phase of equality saturation. Uses multiple-dispatch on rules, Write phase of equality saturation. Application and instantiation of `Patterns` from matching/search results. Definition of `SaturationParams` type, parameters for equality saturation, Definition of equality saturation execution reports. Utility functions and macros to check equality of terms in egraphs.

CONTRIBUTING.md

@@ -10,7 +10,7 @@ A pre-requisite for using Metatheory.jl is to know at least a little about Julia
 
 ## Learning Metatheory.jl
 
-Our [main documentaion](https://github.com/JuliaSymbolics/Metatheory.jl/) provides an overview and some examples of using Metatheory.jl.
+Our [main documentation](https://github.com/JuliaSymbolics/Metatheory.jl/) provides an overview and some examples of using Metatheory.jl.
 The core package is hosted at [Metatheory.jl](https://github.com/JuliaSymbolics/Metatheory.jl/).
 
 ## Before filing an issue

docs/src/rewrite.md

@@ -86,7 +86,7 @@ Matcher pattern may contain slot variables with attached predicates, written as
 - A function that takes a matched expression and returns a boolean value. Such a slot will be considered a match only if `p` returns true.
 - A Julia type. Will be considered a match if and only if the value matching against `x` has a type that is a subtype of `p` (`typeof(x) <: p`)
 
-Similarly `~x::g...` is a way of attaching a predicate `g` to a segment variable. In the case of segment variables `g` gets a vector of 0 or more expressions and must return a boolean value. If the same slot or segment variable appears twice in the matcher pattern, then at most one of the occurance should have a predicate.
+Similarly `~x::g...` is a way of attaching a predicate `g` to a segment variable. In the case of segment variables `g` gets a vector of 0 or more expressions and must return a boolean value. If the same slot or segment variable appears twice in the matcher pattern, then at most one of the occurrence should have a predicate.
 
 For example,
 
@@ -174,7 +174,7 @@ t = comm_monoid ∪ comm_group ∪ distrib
 ## Composing rewriters
 
 Rules may be *chained together* into more
-sophisticated rewirters to avoid manual application of the rules. A rewriter is
+sophisticated rewriters to avoid manual application of the rules. A rewriter is
 any callable object which takes an expression and returns an expression or
 `nothing`. If `nothing` is returned that means there was no changes applicable
 to the input expression. The Rules we created above are rewriters.
@@ -189,7 +189,7 @@ rewriters.
 - `RestartedChain(itr)` like `Chain(itr)` but restarts from the first rewriter once on the
    first successful application of one of the chained rewriters.
 - `IfElse(cond, rw1, rw2)` runs the `cond` function on the input, applies `rw1` if cond
-   returns true, `rw2` if it retuns false
+   returns true, `rw2` if it returns false
 - `If(cond, rw)` is the same as `IfElse(cond, rw, Empty())`
 - `Prewalk(rw; threaded=false, thread_cutoff=100)` returns a rewriter which does a pre-order 
    (*from top to bottom and from left to right*) traversal of a given expression and applies