feat(kernel): add combinator for combining normalizer_extensions

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
fix(build): set LEAN_PATH before make standard and hott libraries

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(build): copy lean executable to bin directory

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
fix(util/lean_path): clear g_lean_path_vector before (re-)initializing it

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(emacs): add shortcut for using --hott option

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
fix(frontends/lean/parser): bug in check_constant_next (when invoked inside of a section)

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
fix(frontends/lean/elaborator): apply coercions in definitions

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

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
fix(frontends/lean/elaborator): use preprocessed expression when displaying errors

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(frontends/lean/pp): pretty print '@' explict operator

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
fix(library/unifier): add a flag to sign that a choice constraint owns a metavariable ?m, that is, it has the right to assign ?m, and the unifier should postpone any other constraint that tries to assign ?m

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
chore(build): eliminate artificial dependencies

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
fix(library/converter): missing constraint on eta expansion

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
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>