时间戳

首页 > 解决方案 > 字符串和 Ascii 的 Coq 导入问题

import - 字符串和 Ascii 的 Coq 导入问题

问题描述

我正在尝试strchr在 Coq 中编写一个简单的函数，然后将其导出到 Haskell。我面临可能与这篇文章（？）类似的导入问题，但我似乎无法解决它们。这是我的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.

标签： importcoq

解决方案

eqb大约一年前添加的，只是 coq 8.9+ 的一部分。你碰巧有旧版本吗？

推荐阅读