search

jesper-bengtson / Charge

Higher-order separation logic framework in Coq
Other
1 stars 1 forks source link

Parsing madness #5

Open jesper-bengtson opened 10 years ago

jesper-bengtson commented 10 years ago

This fails to parse

Notation "'{xml:' e '>'" := e. Eval simpl in {xml:5>.

Notation "'<xml:' e '>'" := e. Eval simpl in xml:5.

This parses successfully.

Notation "'{xml:' e '}'" := e. Eval simpl in {xml:5}.

Notation "'<xml:' e '}'" := e. Eval simpl in <xml:5}.