Build:
traversabletype class (util.data.traversable)- cardinality type classes for types with a finite number of values
and countably many values (
util.data.finite,util.data.countable) categorytype class (util.category)- tactics for proving efficiently inequalities between large literal
numbers (
util.data.norm_num) - machinery for defining coinductive data types
(
util.data.coinductive) - monad for expressing non-terminating computations
(
util.control.monad.non_terminating, now redundant withmathlib) - Various lemmas complementary to the basic libraries