isOccurenceOf -> isOccurrenceOf

Classy.hs

@@ -396,8 +396,8 @@ memberOf x t = x `elem` freeVars t
 occursIn :: (Eq w, v :∈ w) => v -> Term w -> Bool
 occursIn x t = lk x `elem` freeVars t
 
-isOccurenceOf :: (Eq w, v :∈ w) => w -> v -> Bool
-isOccurenceOf x y = x == lk y
+isOccurrenceOf :: (Eq w, v :∈ w) => w -> v -> Bool
+isOccurrenceOf x y = x == lk y
 
 rm :: [v :▹ a] -> [v]
 rm xs = [x | There x <- xs]

Duality.hs

@@ -125,14 +125,14 @@ var = Var . inj
 
 canEta :: Tm Zero → Bool
 canEta (Lam (toExist -> N x (App e1 (Var y)))) = 
-  y `isOccurenceOf` x && not (x `occursIn` e1)
+  y `isOccurrenceOf` x && not (x `occursIn` e1)
 
 {-
 recognize :: Tm Zero → Bool
 recognize t0 = case t0 of 
     Lam f → unpack f $ \x t1 → case t1 of
       Lam g → unpack g $ \y t2 → case t2 of
-        App e1 (Var y) → y `isOccurenceOf` x && 
+        App e1 (Var y) → y `isOccurrenceOf` x &&
                          not (x `occursIn` e1)
         _ → False   
       _ → False   
@@ -557,4 +557,4 @@ instance Insert v a b => Insert v (a ▹ v') (b ▹ v') where
     Here y -> Here y
     There y -> There (There y)
 
--- -}
+-- -}

Talk.hs

@@ -78,16 +78,16 @@ rm :: [a :> v] → [a]
 rm xs = [x | There x <- xs]
 
 occursIn :: (Eq a, v :∈ a) ⇒ v → Tm a → Bool
-occursIn x t = any (`isOccurenceOf` x) (freeVars t)
+occursIn x t = any (`isOccurrenceOf` x) (freeVars t)
 
-isOccurenceOf :: (Eq w, v :∈ w) => w -> v -> Bool
-isOccurenceOf x y = x == inj y
+isOccurrenceOf :: (Eq w, v :∈ w) => w -> v -> Bool
+isOccurrenceOf x y = x == inj y
 
 -- }}}
 -- {{{ η-contract?
 canEta :: Tm Zero → Bool
 canEta (Lam e) = unpack e $ \x t → case t of
-  App e1 (Var y) → y `isOccurenceOf` x && 
+  App e1 (Var y) → y `isOccurrenceOf` x &&
                    not (x `occursIn` e1)
   _ → False
 canEta _ = False

paper/Paper/Context.hs

@@ -140,14 +140,14 @@ contextDoc onlyInCode = do
     reference to a term into a properly tagged de Bruijn index, namely
     the function {|var|}.»
 
-  p"explain isOccurenceOf"
+  p"explain isOccurrenceOf"
    «Conversely, one can implement occurrence-check by combining  {|inj|} with {|(==)|}:
     one first lifts the bound variable to the context of the chosen occurrence and
     then tests for equality.»
 
   [haskellFP|
-  |isOccurenceOf :: (Eq a, v ∈ a) ⇒ a → v → Bool
-  |x `isOccurenceOf` y = x == inj y
+  |isOccurrenceOf :: (Eq a, v ∈ a) ⇒ a → v → Bool
+  |x `isOccurrenceOf` y = x == inj y
   |]
 
   p"occursIn"

paper/Paper/Overview.hs

@@ -315,7 +315,7 @@ overviewDoc onlyInCode = do
   -}
 
   p"canEta"
-   «In the above example, the two functions {|isOccurenceOf|}
+   «In the above example, the two functions {|isOccurrenceOf|}
     and {|freshFor|} use the {|inj|} function to lift {|x|} to
     a reference in the right context before comparing it to the
     occurrences. The calls to these functions do not get more
@@ -327,7 +327,7 @@ overviewDoc onlyInCode = do
   |recognizeExample t0 = case t0 of
   |    Lam f → unpack f $ λ x t1 → case t1 of
   |      Lam g → unpack g $ λ y t2 → case t2 of
-  |        App e1 (Var z) → z `isOccurenceOf` x &&
+  |        App e1 (Var z) → z `isOccurrenceOf` x &&
   |                          x `freshFor` e1 &&
   |                          y `freshFor` e1
   |        _ → False

paper/Paper/Snippets.hs

@@ -20,7 +20,7 @@ apTm =
 canEta =
   [haskellFP|
   |canEta (Lam e) = unpack e $ λ x t → case t of
-  |  App e1 (Var y) → y `isOccurenceOf` x &&
+  |  App e1 (Var y) → y `isOccurrenceOf` x &&
   |                    x `freshFor` e1
   |  _ → False
   |canEta _ = False
@@ -34,7 +34,7 @@ canEtaWithSig =
   [haskellFP|
   |canEta :: Tm Zero → Bool
   |canEta (Lam e) = unpack e $ λ x t → case t of
-  |  App e1 (Var y) → y `isOccurenceOf` x &&
+  |  App e1 (Var y) → y `isOccurrenceOf` x &&
   |                    x `freshFor` e1
   |  _ → False
   |canEta _ = False

paper/Paper/TermStructure.hs

@@ -238,7 +238,7 @@ then apply join inside the structure (using the other higher-order fmap)
   |substitute :: (Monad tm, Eq a, v ∈ a) ⇒
   |              v → tm a → tm a → tm a
   |substitute x t u = u >>= λ y →
-  |     if y `isOccurenceOf` x then t else return y
+  |     if y `isOccurrenceOf` x then t else return y
   |]
 
   -- NP: I changed the names again, I agree that this often the function

paper/main.hs

@@ -441,7 +441,7 @@ So it's easy to see that ∇ is a subtype of ∃ and ∀.
 --  LocalWords:  hereditarycites polymorphism intodo notetodo haskellFP
 --  LocalWords:  notecomm doComment ParItemW startComment stopComment
 --  LocalWords:  commentWhen commentCode unpackCode canEta freshFor
---  LocalWords:  isOccurenceOf canEtaWithSig haskellP Nompa morphism TmB
+--  LocalWords:  isOccurrenceOf canEtaWithSig haskellP Nompa morphism TmB
 --  LocalWords:  fmap isClosed Foldable Traversable untyped VarB AppB
 --  LocalWords:  representable debruijnlambda LamB apB naïve bimap vx
 --  LocalWords:  parameterizes onlyInCode cardinality untag Bifunctor