Remove apply from reg001 since it's in the prelude!
commitcaed480cb4d09a0e5d5076c8b69bf66ff373ab68
authorEdwin Brady <ecb10@st-andrews.ac.uk>
dateSat 18 Jan 2014, 19:52 (13 years ago)
parent865bf99
test/reg001/reg001.idr−3
@@ -1,6 +1,3 @@
1−apply : (a -> b) -> a -> b
2−apply f x = f x
3−
41class Functor f => VerifiedFunctor (f : Type -> Type) where
52 identity : (fa : f a) -> map id fa = fa
63