The concepts macro should require the `WD` field if the `WDID` field is specified and vice versa

UniMath / agda-unimath

The agda-unimath library

https://unimath.github.io/agda-unimath/

MIT License

222 stars 71 forks source link

The concepts macro should require the `WD` field if the `WDID` field is specified and vice versa #1076

Closed fredrik-bakke closed 7 months ago

fredrik-bakke commented 8 months ago

If either data point is specified, the other one should also be possible to determine, and making them corequired will avoid incomplete specifications.