Coq导入Strings和Ascii的问题

Question

我正在尝试在Coq中编写一个简单的strchr函数，然后将其导出到Haskell。我面临的导入问题可能类似于this post（？），但我似乎无法解决它们。这是我的coq代码：

(***********)
(* IMPORTS *)
(***********)
Require Import Coq.Arith.PeanoNat.
Require Import Coq.Lists.List.
Require Import Coq.Strings.String.
Require Import Coq.Strings.Ascii. 

(**********)
(* strchr *)
(**********)
Fixpoint strchr (haystack : string) (needle : ascii) : string :=
  match haystack with
  | EmptyString => EmptyString
  | String c s' => match (Ascii.eqb needle c) with
                   | true => s
                   | false => strchr s' needle
                   end
  end.

(********************************)
(* Extraction Language: Haskell *)
(********************************)
Extraction Language Haskell.

(***************************)
(* Extract to Haskell file *)
(***************************)
Extraction "/home/oren/GIT/kMemLoops/strchr.hs" strchr.

这是我得到的错误：

Error: The reference Ascii.eqb was not found in the current environment.

Answer 1

eqb添加了about a year ago，只是coq 8.9+的一部分。你碰巧有旧版本吗？