refactor(library/standard): use new coding style, rename bool.b0 and bool.b1 to bool.ff and bool.tt

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

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
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>
added various auxiliary definitions to fundef
continue fundef
modified emacs mode to build with local system
Added a file for cantor's paradox.
better breaking cases for cantor
Added a crash test case.