The Coq mailing list

[t x <txrev319 AT gmail.com>]

With apologies for my ignorance, I still can't get it to work. For example:

https://gist.github.com/anonymous/6651830

What am I doing wrong? I'm almost verbatim copying theories/String.v :

== Part of String.v

(** *** Definition of strings *)

(** Implementation of string as list of ascii characters *)

Inductive string : Set :=
  | EmptyString : string
  | String : ascii -> string -> string.

Delimit Scope string_scope with string.
Bind Scope string_scope with string.
Local Open Scope string_scope.
)

== End

On Sat, Sep 21, 2013 at 1:53 PM, Vincent Laporte <vincent.laporte AT gmail.com> wrote:

Le 2013-09-21 15:43, t x a écrit :

>   I'm trying to use Notation together with Scopes.
>
>   The following is a minimal example which fails
>
>
> Inductive foo := fA | fB.
> Variable fAdd : foo -> foo -> foo.
>
> Notation "A + B" := (fAdd A B) : foo_scope.
>
> Check (fA + fB) % foo_scope.
>
>>>> Error: Unknown scope delimiting key foo_scope.

Hi,

Looking for “delimiting key” in the manual should help.

http://coq.inria.fr/distrib/current/refman/Reference-Manual014.html#hevea_command262

--
Vincent.