issues
search
UniMath
/
agda-unimath
The agda-unimath library
https://unimath.github.io/agda-unimath/
MIT License
222
stars
71
forks
source link
Enhancements for the Concepts macro
#1093
Closed
VojtechStep
closed
7 months ago
VojtechStep
commented
7 months ago
This PR:
Makes concepts throw an error when a wikidata ID is provided without a label. Fixes #1076
Uses lowercase wikidata labels in the concept tags, and only capitalizes them when generating links. Fixes #1077
Disallows newlines in quoted parts of the macro. Fixes #1092
Correctly finds Agda definitions which have single-quotes in them. Fixes #1075
Adds "(disambiguation)" to concept names in the database, when a disambiguation is provided
This PR: