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(frontends/lean/pp): improve let-expr pretty printer

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(bin/linja): add linja

close #103, #108
feat(emacs/lean-settings): use linja for flycheck
chore(library/.gitignore): update
chore(library): add .project file
fix(frontends/let): let-expression pretty printer

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(build): invoke linja from lean build

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(frontends/lean/dependencies): do not stop computing dependencies at error, compute as many as possible, and sign error in the end

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(frontends/lean/server): add 'OPTIONS' command to 'lean --server'

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>