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.
Last updated: Oct 03 2023 at 04:02 UTC