Twan van Laarhoven wrote:
Robin Green wrote:
I am proving various statements relating to applicative functors, using
the Coq proof assistant (I am considering only Coq terms, which always
terminate so you don't have to worry about _|_). However, I'm not sure
how to go about proving a certain
Isaac Dupree wrote:
Unfortunately, I get puzzling type errors if I annotate either one of
them with their type (e.g.
(Applicative f) = f (a - b) - f a - f (Int, b)
) in an expression. The very answer doesn't seem to typecheck.
:t \f x - fmap ((,) (0::Int)) (f * x) :: (Applicative f) = f (a1
Twan van Laarhoven wrote:
Isaac Dupree wrote:
Unfortunately, I get puzzling type errors if I annotate either one of
them with their type (e.g.
(Applicative f) = f (a - b) - f a - f (Int, b)
) in an expression. The very answer doesn't seem to typecheck.
:t \f x - fmap ((,) (0::Int)) (f * x)
I am proving various statements relating to applicative functors, using
the Coq proof assistant (I am considering only Coq terms, which always
terminate so you don't have to worry about _|_). However, I'm not sure
how to go about proving a certain conjecture, which, translated back
into Haskell
Robin Green wrote:
I am proving various statements relating to applicative functors, using
the Coq proof assistant (I am considering only Coq terms, which always
terminate so you don't have to worry about _|_). However, I'm not sure
how to go about proving a certain conjecture, which,
