refactor(library/sigma): fix/use sigma notation
feat(frontends/lean/pp): add option 'pp.numerals'
fix(frontends/lean/token_table): increase binding power of decreasing operator
feat(library/util): add auxiliary functions for creating tuples (using sigma types)
feat(kernel/type_checker): add ensure_type variant
feat(frontends/lean): type check 'decreasing' proofs in definition using well-founded recursion
feat(library/init/logic): add is_true and is_false
feat(util/buffer): add insert method
feat(frontends/lean/elaborator): replace metavariables in the equation lhs with fresh local constants before invoking compiler
fix(tests/lean/interactive): adjust test to reflect changes in the standard library
refactor(library/init/sigma): simplify lex.accessible proof using 'cases' tactic
refactor(library/init/logic): move theorems to logic/cast
refactor(library/init/logic): move theorems to library/logic
refactor(library/init): move more theorems to logic
test(tests/lean/extra): more tests for equation elaborator
feat(library/algebra/ordered_ring): start on ordered_ring, and minor changes elsewhere
refactor(library/algebra/ordered_ring): add workarounds to improve performance
fix(frontends/lean/structure_cmd): simplify structure names
fix(library/init/logic): expose inhabited basic instances
fix(library/aliases): aliases in sections and contexts