UniMath / agda-unimath

The agda-unimath library
https://unimath.github.io/agda-unimath/
MIT License
222 stars 71 forks source link

Feature additions – unused imports #1180

Closed fredrik-bakke closed 2 months ago

fredrik-bakke commented 2 months ago
EgbertRijke commented 2 months ago

I can't really judge this code, but I am happy with the idea of this addition

fredrik-bakke commented 2 months ago

Then I think it's good to merge 😄

EgbertRijke commented 2 months ago

We got auto-merge on on the colocal pull request, so I'm going to turn this one off because it needs to be updated anyway

EgbertRijke commented 2 months ago

Ah, I didn't see that it just merged

fredrik-bakke commented 2 months ago

Oh, sorry about that