CODEWITHSUNDEEP
formatcoqnotation
Ptival
Ptival

Reputation: 9437

Coq notation format for double square braces

According to the documentation, one can define formats for printing notations: https://coq.inria.fr/refman/Reference-Manual014.html#sec530

However, one can define a notation such as:

Notation " '[[' a ']]' b " := (* something *).

It is very unclear whether the two can interact. Trying:

format " '[hv' '[[' a ']]' ']' b "

for instance, trips Coq up as it expects a square brace to be followed by one of , v, and hv.

Any other sort of escaping I have tried so far made Coq refuse the format as not matching the notation.

I'm not sure this can be done...

Upvotes: 1

Views: 199

Answers (1)

ejgallego
ejgallego

Reputation: 6852

Your friend here is metasyntax:parse_format https://github.com/coq/coq/blob/trunk/toplevel/metasyntax.ml#L102

As you can see in the code, your concrete scheme is not going to work. I dunno if there could be some specific hack, for now you'll have to desist using double brackets.

I am certain however that a patch adding a case for [[ in parse_quoted would be considered by Coq upstream.

Hopefully 8.7 will bring some improvements here, CEP#9 tries to propose replacing/evolving unparsing to a true box-based model.

Upvotes: 2

Related Questions