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?