search

HoTT / Coq-HoTT

A Coq library for Homotopy Type Theory
http://homotopytypetheory.org/
Other
1.25k stars 193 forks source link

fix universes in Vector.v #1980

Closed Alizter closed 4 months ago

Alizter commented 4 months ago

This was creating too many universe variables before. We also make sure that Matrix only takes the universe of the type of elements.