refactor(*): add uniform names for "meta-objects"
fix(library/data/int): define sub from algebra.sub
fix(data/int/basic): move decidable theorems
fix(tests/lean/run): replace "open [notation]" with "open [notations]"
feat(util/list): add to_list from buffer
refactor(library/util): allow mk_telescopic_eq to be used with (terms, locals)
feat(library/util): add mk_heq
feat(library/util): add mk_refl
feat(hott/init): add proof for Hedberg's theorem
feat(hott/init): add auxiliary definition needed by definitional package
refactor(frontends/lean): move choice_iterator to library
refactor(frontends/lean): move type_checker_ptr typedef to library
refactor(frontends/lean): move pp_options to library
refactor(frontends/lean/placeholder_elaborator): reduce coupling between placeholder_elaborator and frontends/lean
refactor(frontends/lean): move some auxiliary procedures to library/tactic
refactor(frontends/lean): move placeholder_elaborator to library/tactic
feat(hott/init/datatypes): add sum.intro_left and sum.intro_right aliases
refactor(library/init/datatypes): change implicit arguments of sum.inl and sum.inr
refactor(library/init/sigma): rename sigma.dpair->sigma.mk, sigma.dpr1->sigma.pr1, sigma.dpr2->sigma.pr2
refactor(hott): use same name convention for sigma in the HoTT and standard libraries