Single rule which captures all of eta conversion for functions. But I'm not sure if it is sound

Author: diode-lang

src/Agda/Core/Checkers/Converter.agda

@@ -244,9 +244,18 @@ convertWhnf r (TSort s) (TSort t) = convSorts s t
 --     -- (x : Name) (f : NameIn α)
 --     -- (b : Term x ▸ α) (proof : b ≅ TApp (TVar depPairF) (TVar depPairX) )
 --     return (CEtaVar x f b proof)
-convertWhnf r (TVar f) (TLam x b) = {!!}
-convertWhnf r (TLam x v) (TVar x') = tcError "implement eta-functions 2"
-convertWhnf r (TApp _ _) (TLam _ _) = tcError "implement eta-functions 3"
+convertWhnf r functionTerm (TLam x b) = 
+  let 
+  depPairX = ⟨ x ⟩ (Zero ⟨ IsZero refl ⟩)
+  subsetProof = (subWeaken subRefl)
+  newScope = singBind r
+  term = TApp (weakenTerm subsetProof functionTerm) (TVar depPairX)
+  in
+  do
+    conversionProof <- convertCheck newScope b term
+    return (CEtaVar2 x functionTerm b conversionProof)
+-- convertWhnf r (TLam x v) (TVar x') = tcError "implement eta-functions 2"
+-- convertWhnf r (TApp _ _) (TLam _ _) = tcError "implement eta-functions 3"
 convertWhnf r _ _ = tcError "two terms are not the same and aren't convertible"
 
 {-# COMPILE AGDA2HS convertWhnf #-}