Stream: Coq users

Topic: Running mystery function unknown interpretation

alexm98 (Jun 11 2020 at 13:41):

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.

Karl Palmskog (Jun 11 2020 at 13:44):

You need to add From Coq Require Import List. just above.

Kenji Maillard (Jun 11 2020 at 13:45):

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

Require Import Coq.Lists.List.
Import ListNotations.

alexm98 (Jun 11 2020 at 13:48):

Yes! thanks!

Last updated: Oct 03 2023 at 04:02 UTC