Coq Импорт проблем со строками и Ascii - PullRequest
Новая
       14

Coq Импорт проблем со строками и Ascii

1 голос
/ 01 мая 2019

Я пытаюсь написать простую 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.

1 Ответ

2 голосов
/ 01 мая 2019

eqb был добавлен около года назад и является только частью coq 8.9+. У вас есть старая версия?

...