Marks place in code where eta-functions conversion should happen ; Add two more counterexamples for eta-functions ; spelling fixes

Author: diode-lang

src/Agda/Core/Checkers/Converter.agda

@@ -229,7 +229,9 @@ convertWhnf r (TCase d ri u bs rt) (TCase d' ri' u' bs' rt') =
   convertCase r d d' ri ri' u u' bs bs' rt rt'
 convertWhnf r (TPi x tu tv) (TPi y tw tz) = convPis r x y tu tw tv tz
 convertWhnf r (TSort s) (TSort t) = convSorts s t
---let and ann shoudln't appear here since they get reduced away
+--let and ann shouldn't appear here since they get reduced away
+convertWhnf r (TVar _) (TLam _ _) = tcError "implement eta-functions 1"
+convertWhnf r (TLam x v) (TVar x') = tcError "implement eta-functions 2"
 convertWhnf r _ _ = tcError "two terms are not the same and aren't convertible"
 
 {-# COMPILE AGDA2HS convertWhnf #-}

src/Agda/Core/Checkers/TypeCheck.agda

@@ -87,7 +87,7 @@ inferCase {α = α} ctx d rixs u bs rt = do
 
   El s tu , gtu ← inferType ctx u
   d' , (params , ixs) ⟨ rp ⟩ ← reduceToData r tu
-    "can't typecheck a constrctor with a type that isn't a def application"
+    "can't typecheck a constructor with a type that isn't a def application"
   Erased refl ← convNamesIn d d'
   df ⟨ deq ⟩ ← tcmGetDatatype d
   let ds : Sort α

src/Agda/Core/Rules/Unification.agda

@@ -14,8 +14,8 @@ private open module @0 G = Globals globals
                                    {- PART ONE : Shrinking -}
 ---------------------------------------------------------------------------------------------------
 module Shrinking where
-  {- A module where shrinking, an operation to remove some variables of a scope while
-    preserving dependancies is defined -}
+  {- A module where shrinking is defined, which is an operation to remove some variables of a scope while
+    preserving dependencies-}
 
   private variable
     @0 x : Name

test/EtaFunctionsChurchWithConst.agda

@@ -10,5 +10,12 @@ const = λ A → λ x → λ y → x
 eta-functions_expl : (A B : Set) (f : A → B) → (Id (A → B) f (λ x → (f (const A x x))))
 eta-functions_expl = λ A B → λ f → refl (A → B) f
 
+eta-functions_two : (A B : Set) (f : A → B) → 
+    (Id (A → B) (λ x → (f (const A x x))) (λ v → (λ w → (f w)) v) )
+eta-functions_two = λ A B → λ f → refl (A → B) f
+
+eta-functions_three : (A B : Set) (f : A → B) → 
+    (Id (A → B) (λ v → (λ w → (f w)) v) (λ x → (f (const A x x))) )
+eta-functions_three = λ A B → λ f → refl (A → B) f