test(tests/lean/run): add test

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(util): add sequence object with O(1) concatenation operation

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
chore(*): create alias for std::pair

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
refactor(kernel/type_checker): remove "global" constraint buffer from type_checker, and use constraint_seq instead

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
fix(library/unifier): missing set_conflict

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
chore(library/standard): remove workarounds

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(library/unifier): allow computation when solving flex-rigid constraints

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
refactor(library/unifier): make it easier to add new options to the unifier

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(library/standard/data/quotient): import quotient from lean 0.1
feat(library/standard): port int, and reorganize a lot
fix(lean/library/standard): fix tests, more cleanup
feat(library/standard/data/nat/div): port div
fix(library/unifier): remove incorrect assertion, a local constant may occur in the type of a metavariable that was not instantiated yet

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
fix(doc/lean/tutorial): adjust tutorial to library changes, fix test

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
chore(library/standard/data/int/basic): remove TODO's that were addressed by recent improvements

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
fix(tests/util/sequence.cpp): clang build error
feat(library/standard/data/nat/order): add le_decidable, lt_decidable, ge_decidable, gt_decidable

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
chore(library/standard/data/nat/order): remove unnecessary 'proofs'

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
fix(frontends/lean/pp): bug when pretty printing binder information, fixes #73

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
fix(emacs): roll back to generic mode