Commit 6f623030 authored by Matthew Pickering's avatar Matthew Pickering Committed by Ben Gamari
Browse files

Remove unused function: mkFunCos

Reviewers: goldfire, bgamari, dfeuer

Reviewed By: dfeuer

Subscribers: dfeuer, thomie, carter

Differential Revision: https://phabricator.haskell.org/D4587
parent f78df87c
......@@ -31,7 +31,7 @@ module Coercion (
mkPiCo, mkPiCos, mkCoCast,
mkSymCo, mkTransCo,
mkNthCo, mkLRCo,
mkInstCo, mkAppCo, mkAppCos, mkTyConAppCo, mkFunCo, mkFunCos,
mkInstCo, mkAppCo, mkAppCos, mkTyConAppCo, mkFunCo,
mkForAllCo, mkForAllCos, mkHomoForAllCos, mkHomoForAllCos_NoRefl,
mkPhantomCo,
mkUnsafeCo, mkHoleCo, mkUnivCo, mkSubCo,
......@@ -553,10 +553,6 @@ mkFunCo r co1 co2
= Refl r (mkFunTy ty1 ty2)
| otherwise = FunCo r co1 co2
-- | Make nested function 'Coercion's
mkFunCos :: Role -> [Coercion] -> Coercion -> Coercion
mkFunCos r cos res_co = foldr (mkFunCo r) res_co cos
-- | Apply a 'Coercion' to another 'Coercion'.
-- The second coercion must be Nominal, unless the first is Phantom.
-- If the first is Phantom, then the second can be either Phantom or Nominal.
......
......@@ -33,8 +33,6 @@ mkKindCo :: Coercion -> Coercion
mkSubCo :: Coercion -> Coercion
mkProofIrrelCo :: Role -> Coercion -> Coercion -> Coercion -> Coercion
mkFunCos :: Role -> [Coercion] -> Coercion -> Coercion
isReflCo :: Coercion -> Bool
isReflexiveCo :: Coercion -> Bool
decomposePiCos :: Kind -> [Type] -> Coercion -> ([Coercion], Coercion)
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment