fix(frontends/lean/elaborator): bug in the elaborator reported by Jeremy

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(library/standard): add or_comm, and_comm, ... theorems, cleanup notation

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
fix(frontends/lean/elaborator): bug when mixing implicit arguments and sections

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
chore(kernel/replace_fn): add syntax sugar for replace function

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
fix(library/choice): we should be able to store 'choice' operators in .olean files, this can happen because of notation decls

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(kernel/constraint): add 'print' function for debugging purposes

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(library/standard): add equivalence inductive predicate

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
fix(library/module): module index assignment

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
refactor(kernel/error_msgs): move pp_type_mismatch to error_msgs module

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(library/unifier): improve error message when metavar assignment is type incorrect

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(library/standard/bit): add theorems and notation

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

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(library/standard): add more decidable instances

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
chore(frontends/lean): add 'replace' auxiliary funcs

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
fix(library/choice): style

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(library/standard/if): cleanup 'if-then-else' theorems

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(library/standard/bool_decidable): cleanup bool_decidable, and remove the artificial dependency to bit

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
fix(library/module): sign error is circular module dependency is detected

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
perf(build): use make -j option when invoking external makefile for compiling Lean libraries

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(util/lean_path): allow 'import dirname' as shorthand for 'import dirname.default'

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