0

In CoqId I have written the following:

Parameter i: Type. (* Type for worlds *)
Parameter u: Type. (* Type for individuals *)
Definition o := i -> Prop. (* Type of modal propositions *)

Parameter r: i -> i -> Prop. (* Accessibility relation for worlds *)

Definition A {t: Type}(p: t -> o)(w: i) := forall x, p x w. 
Notation "’mforall’ x , p" := (A (fun x => p))
(at level 200, x ident, right associativity) : type_scope. 
Notation "’mforall’ x : t , p" := (A (fun x:t => p))
(at level 200, x ident, right associativity, format"[’’mforall’’/’ x : t,’/’ p’]’")
: type_scope. 

This produces the error The format does not match the notation. with "[’’mforall’’/’ highlighted in red.

What is the problem here and how can I solve it?

1 Answer 1

1

You need spaces around tokens. At least one space for the format to be valid, then extra spaces that are preserved in the output (otherwise your tokens are going to be mushed together).

Parameter i: Type. (* Type for worlds *)
Parameter u: Type. (* Type for individuals *)
Definition o := i -> Prop. (* Type of modal propositions *)

Parameter r: i -> i -> Prop. (* Accessibility relation for worlds *)

Definition A {t: Type}(p: t -> o)(w: i) := forall x, p x w. 
Notation "'mforall' x , p" := (A (fun x => p))
(at level 200, x ident, right associativity) : type_scope. 
Notation "'mforall' x : t , p" := (A (fun x:t => p))
(at level 200, x ident, right associativity, format"'[' 'mforall'  '/' x  :  t ,  '/  ' p ']'")
: type_scope. 

(* example *)
Check A (fun zzzzzzzzzzzzzzzzzzzzzzzzzzzzzzzzzzzzz => eq zzzzzzzzzzzzzzzzzzzzzzzzzzzzzzzzzzzzz).

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.