git.iko.soy/Idris-dev
on master help sign in
Remove apply from reg001 since it's in the prelude!
caed480Edwin Brady
test/reg001/reg001.idr−3
compare with master
unifiedsplit
@@ -1,6 +1,3 @@
1−apply : (a -> b) -> a -> b
2−apply f x = f x
3−
4class Functor f => VerifiedFunctor (f : Type -> Type) where
1class Functor f => VerifiedFunctor (f : Type -> Type) where
5 identity : (fa : f a) -> map id fa = fa
2 identity : (fa : f a) -> map id fa = fa
6
3