I was trying to use `fmap`

from coq-ext-lib. So I tried:

```
Require Import ExtLib.Structures.Functor.
Import FunctorNotation.
Compute (S <$> Some 2).
(*
= match ?Functor with
| {| fmap := fmap |} => fmap
end nat nat (fun x : nat => S x) (Some 2)
: option nat
*)
Check (S <$> Some 2).
(*
S <$> Some 2
: option nat
where
?Functor : [ |- Functor option]
*)
```

I was hoping to get `Some 3`

out of `S <$> Some 2`

. What am I missing here?

Is it because of some type class?

`fmap`

's type is like:

```
Check fmap.
(*
fmap
: (?A -> ?B) -> ?F ?A -> ?F ?B
where
?F : [ |- Type -> Type]
?Functor : [ |- Functor ?F]
?A : [ |- Type]
?B : [ |- Type]
*)
```

Wouldn't giving `S: nat -> nat`

make `A`

and `B`

to be nat? With `option`

as `F`

?

yes that's exactly what happens: in `(S <$> Some 2)`

, `?F`

is unified with `option`

while `?A,?B`

are unified with `nat`

. The problem is that the `?Functor`

argument is still missing.

I guess you should either define an instance of `Functor option`

, or maybe it already exists somewhere in extlib but is not accessible with the specific imports you used.

Thanks.

I did

```
Require Import ExtLib.Data.Option. │
```

(still not sure if that's the right package, but it works.)

and then

```
Compute (S <$> Some 2).
```

gave `Some 3`

.

Julin S has marked this topic as resolved.

Last updated: Jan 29 2023 at 01:02 UTC