feat(library/hott): add more hott definitions

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
fix(library/unifier): tolerate exceptions in the type_checker::infer method. This can happen since when we try projections we don't check whether they are type correct

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
fix(library/unifier): bug in process_delta

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
perf(kernel/converter): improve is_def_eq_binding

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
perf(kernel/type_checker): improve infer_lambda performance

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
perf(kernel/expr): use thread local deletion buffer

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
fix(kernel/replace): make sure 'replace' is reentrant

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
perf(library/unifier): minimize the number of constraints generated in the flex_rigid 'imitation' step

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
perf(kernel/instantiate): add custom instantiate for 'easy' cases

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
perf(kernel/expr): inline get_free_var_range, and cache its value for local and metavars

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
fix(kernel/type_checker): error message

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(library/hott): add more definitions and theorems from the HoTT book

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(frontends/lean/decl_cmds): allow parameters with different types to be declared using the same 'parameters' command

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

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(library/hott): use new 'parameters' command

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
chore(CMakeLists.txt): mark gmp and mpfr as required packages
chore(.travis.osx.yml): use homebrew gcc-4.8.3
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>