feat(library/data/nat): mark more arguments implicit

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
refactor(library): more implicit_args for: and_assoc, and_comm, or_assoc, or_comm, if_pos, if_neg

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
fix(src/emacs/lean-syntax.el): remove obsolete command set_opaque

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(src/emacs/lean-syntax.el): add commonly used operators

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
chore(library): minor cleanup

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
refactor(library/unifier): cleanup mk_macro_imitation

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

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
fix(kernel/converter): missing case

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(frontends/lean): avoid exponential blowup when processing let-expressions with a lot of sharing, cleanup show-expression

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(library/unifier): remove mk_macro_imitation, we instead expand the macro before solving flex-rigid constraints

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
refactor(library): move more notation to general_notation
feat(library/data/nat/div.lean): remove dependence on funext
fix(library/nat/div): remove unnecessary '_''s

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
fix(frontends/lean/elaborator): missing '\n' in error message

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
fix(frontends/lean/pp): pretty print 'let-expressions', closes #87

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
fix(frontends/lean/pp): remove unreachable code: elaborator eliminates typed_expr macros

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(bin/linja): add linja
lean-mode checkpoint
chore(library/.gitignore): update