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>
feat(library/standard/logic): iff is refl, trans, and symm

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(library/standard): add Diaconescu's theorem

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
fix(util/rc): reference counter memory_order flags

See discussion at
http://www.chaoticmind.net/~hcb/projects/boost.atomic/doc/atomic/usage_examples.html#boost_atomic.usage_examples.example_reference_counters
http://stackoverflow.com/questions/10268737/c11-atomics-and-intrusive-shared-pointer-reference-count

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