UniMath/agda-unimath

Undetected ill-formed macro invocations

fredrik-bakke opened this issue · 0 comments

I see some ill-formed concept macro invocations are slipping through the cracks, such as the following in synthetic-catetegory-theory.equivalences-synthetic-categories:

{{#concept "equivalence" Disambiguation="Synthetic categories}}

surely such invocations should not be accepted and should rather throw an error.