2 commits

Author	SHA1	Message	Date
Floris van Doorn	e5d5ef9d55	feat(hott/library): various changes and additions. ... Most notably: Give le.refl the attribute [refl]. This simplifies tactic proofs in various places. Redefine the order of trunc_index, and instantiate it as weak order. Add more about pointed equivalences.	2016-03-03 10:13:20 -08:00
Jeremy Avigad	27865e1c8b	feat(library/algebra/order_bigops): add min and max over finsets and finite sets	2016-01-24 16:26:57 -08:00