Closed isovector closed 3 years ago
data Foo a = Done a | Rec (Foo a) instance Functor Foo where fmap = (\ fab fa -> case fa of (Done a) -> Done (fab a) (Rec fa2) -> fmap fab fa2)
this last case should be Rec (fmap fab fa2)
Rec (fmap fab fa2)
This is automatically resolved by the known fmap tactic, so I think we're fine.
known fmap
this last case should be
Rec (fmap fab fa2)