Hi everyone. I want to use finmap in a project, but I am having trouble using it.

The doc on Github says that a finmap can be constructed by using `[fmap x : S => E]`

. But this doesn't work for me.

For example, when I use the command `Check [fmap x : bool => ~~ x]%fmap.`

to check the type of this term, I got the following error:

`Error: The term "[ffun x => ~~ x]" has type "{ffun bool_finType -> bool"}, while it is expected to have type "{ffun ?domf -> ?V".`

I have checked that the library version (1.5.0) and Coq version (8.12.0) are both ok, I don't know why Coq cannot unify these two types. Can someone help me? Any suggestions would be appreciated.

Did you import `choice`

?

Yes, I import `all_reflect`

, which includes `choice`

.

Here is a minimal example.

```
From mathcomp Require Import finmap.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Check [fmap x : bool => ~~ x].
```

It seems to me that there is a bug in the `[fmap _ => _]`

notation or with the coercion from fsets to Sortclass. @Cyril Cohen

(If I understand correctly, the problem is that the domain of a `fmap`

is a `fset`

rather than a `Type`

, and there should be a coercion from `fset`

to `Type`

, but somehow this does not work. But I'm not familiar with this part of the library and might be wrong.)

The domain `S`

is supposed to be a `fset`

not a type.

I'm wondering why you are using a fmap here, since the domain is a fintype, a finfun is better...

```
Check [ffun x => ~~ x].
```

If you are insisting on using (mathcomp) finmap, then you would have to write

```
Check [fmap x : [fset b : bool | true] => ~~ val x].
```

BTW, this is a mathcomp question, so I'm moving this to the mathcomp stream.

This topic was moved here from #Miscellaneous > Finmap construction by Cyril Cohen

Well, this simple example here is a simplified version of the problem I actually have. What I actually want to do is to initialize a fmap `{fmap K -> V}`

using a function of type `K -> V`

, and this fmap may be changed afterward.

Anyway, thanks a lot for your help!

Maybe you are looking for `fsfun`

instead then...

Ok, thanks for your advice!

Last updated: Jul 15 2024 at 21:02 UTC