on master help sign in
Merge pull request #4178 from joom/master

Add Functor implementation for FunClause and FunDefn

commitd6c48eee721801caa077c63bc78a8364c2653f44 authorDavid Christiansen <david@davidchristiansen.dk> dateMon 6 Nov 2017, 07:47 (9 years ago) parentf3dcca52e0a1c8
1 file changed+8−1
libs/base/Language/Reflection/Utils.idr+8−1
libs/base/Language/Reflection/Utils.idr+8−1
@@ -308,7 +308,7 @@ implementation Show Raw where
308308 my_show d (RApp tm tm') = assert_total $ showCon d "RApp" $ " " ++ my_show App tm ++ " " ++ my_show App tm'
309309 my_show d RType = "RType"
310310 my_show d (RConstant c) = assert_total $ showCon d "RConstant" $ showArg c
311− my_show d (RUType u) = "RUType"
311+ my_show d (RUType u) = "RUType"
312312
313313
314314implementation Show Err where
@@ -387,3 +387,10 @@ implementation Show tm => Show (FunClause tm) where
387387 showCon d "MkFunClause" $ showArg lhs ++ showArg rhs
388388 showPrec d (MkImpossibleClause lhs) =
389389 showCon d "MkImpossibleClause" $ showArg lhs
390+
391+implementation Functor FunClause where
392+ map f (MkFunClause lhs rhs) = MkFunClause (f lhs) (f rhs)
393+ map f (MkImpossibleClause lhs) = MkImpossibleClause (f lhs)
394+
395+implementation Functor FunDefn where
396+ map f (DefineFun n clauses) = DefineFun n (map (map f) clauses)