Nick Rioux
Nick Rioux
It would be nice to be able to format metavariables differently than constants and other parts of the language. For example: λ _x_ : _τ_ . if _e_ then _e₁_...
My AS2-generated file contains the line: ```coq Notation "[ sigmaval ]" := (subst_tm sigmaval) (at level 1, left associativity, only printing) : fscope. ``` Unfortunately, this notation conflicts with the...