lean4-htt/library/data/rbtree
2017-11-17 22:59:50 -08:00
..
default.lean refactor(library): rbtree lemmas do not need to be in init folder 2017-11-17 16:14:28 -08:00
lemmas.lean refactor(library/init/data/rbtree): rbtree does not need (decidable_rel lt) parameter 2017-11-17 22:59:50 -08:00