refactor(frontends/lean): rename action::is_compatible to action::is_equal

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(frontends/lean): allow user to provide a terminator for 'foldr' and 'foldl'

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
fix(frontends/lean): remove keywords 'class' and '[class]'

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(build): add 'clean-olean' custom-target

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
fix(frontends/lean/parser.cpp): fix typo
feat: add "--flycheck" option to print out error msgs for flycheck
fix(kernel/converter): missing constraints

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
refactor(library/unifier): process_flex_rigid method before adding yet another case split

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(library/error_handling): add flycheck_scope helper class

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
chore(shell/CMakeLists.txt): put EXECUTABLE_SUFFIX to lean
chore(CMakeLists.txt): replace "lib1;lib2" with "lib1" "lib2"
fix(library/unifier): bug that was making unifier miss solutions, and add a new case-split that tries to solve flex_rigid constraints by putting the rhs into whnf

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(library/unifier): add flag for enabling/disabling expensive extensions in the unifier

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(frontends/lean/pp): do not display metavariable arguments by default, add option pp.metavar_args to control whether they are displayed or not

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
fix(emacs): syntax highlight issues reported by Jeremy

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(library/error_handling): add helpers classes for creating WARNING and INFO annotations for flycheck

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

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
fix(frontends/lean/parser): generate flycheck-friendly import error

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(frontends/lean): add --flyinfo option

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
fix(frontends/lean/dependencies): warning message

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