File tree Expand file tree Collapse file tree 1 file changed +0
-5
lines changed
Expand file tree Collapse file tree 1 file changed +0
-5
lines changed Original file line number Diff line number Diff line change @@ -239,16 +239,11 @@ convertWhnf r functionTerm (TLam x b) =
239239 do
240240 conversionProof <- convertCheck newScope b term
241241 return (CEtaFunctions x functionTerm b conversionProof)
242- <<<<<<< HEAD
243242convertWhnf r a b = do
244243 conversionProof <- convertCheck r b a
245244 return (CSym conversionProof)
246245-- convertWhnf r (TLam x v) (TVar x') = tcError "implement eta-functions 2"
247246-- convertWhnf r (TApp _ _) (TLam _ _) = tcError "implement eta-functions 3"
248- =======
249- convertWhnf r (TLam x v) (TVar x') = tcError "implement eta-functions 2"
250- convertWhnf r _ _ = tcError "two terms are not the same and aren't convertible"
251- >>>>>>> a146e6c (Working example for function eta-conversion where TLam is on left and TVar is on right)
252247
253248{-# COMPILE AGDA2HS convertWhnf #-}
254249
You can’t perform that action at this time.
0 commit comments