Hello everyone, I'm trying to run this function in Coq to see what it does, but I get "Unknown interpretation for _ :: _ ".

```
Fixpoint mistery (A : Type)(m : list bool)(s : list A) :=
match m, s with
| b :: m', x :: s' => if b then x :: mistery A m' s' else mistery A m' s'
| _, _ => nil
end.
```

You need to add `From Coq Require Import List.`

just above.

And probably also import the notations (Edit: actually only needed if you just import the submodule)

```
Require Import Coq.Lists.List.
Import ListNotations.
```

Yes! thanks!

Last updated: Oct 03 2023 at 04:02 UTC