So I'm really new to coq, functional programming altogether, and I'm trying to express the topological definition of continuity in coq. I'm using this code to define a topology in coq. My best attempt at expressing continuity given a particular function is,
Definition Continuous (X:Type)(TX:Topology X)(Y:Type)(TY:Topology Y)(f:X->Y):=
forall V, exists U, all y:V, some x:U, f x = y.
I'm getting the error
"The term "f x" has type "Y" while it is expected to have type "Prop".
No idea what to do, any help is appreciated.
The problem is that Coq's parser was interpreting y wrong. I was able to fix the problem by changing the notation for all and some a little bit:
Notation "'all' x 'in' U , P" := (forall x, U x -> P) (at level 200).
Notation "'some' x 'in' U , P" := (exists x, U x /\ P) (at level 200).
Definition continuous (X:Type)(TX:topology X)(Y:Type)(TY:topology Y)(f:X->Y):=
forall V, exists U, all y in V, some x in U, f x = y.
Notice how the notation levels are different and how it uses the in keyword instead of :. I don't know if there's a way of getting : to work; Coq 8.5 kept complaining if I tried to.