diff options
Diffstat (limited to 'src/Encoded/Pair.idr')
| -rw-r--r-- | src/Encoded/Pair.idr | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/src/Encoded/Pair.idr b/src/Encoded/Pair.idr index 5873e40..4b66cfe 100644 --- a/src/Encoded/Pair.idr +++ b/src/Encoded/Pair.idr @@ -39,6 +39,11 @@ bimap = Abs $ Abs $ Abs $ Abs $ ] export +mapFst : {ty1, ty1', ty2 : Ty} -> Term ((ty1 ~> ty1') ~> ty1 * ty2 ~> ty1' * ty2) ctx +mapFst = AbsAll [<_,_] (\[<f, x] => + App pair [<App (f . fst) [<x], App snd [<x]]) + +export mapSnd : {ty1, ty2, ty2' : Ty} -> Term ((ty2 ~> ty2') ~> ty1 * ty2 ~> ty1 * ty2') ctx mapSnd = Abs $ Abs $ let f = Var (There Here) in |