feat(kernel/environment): add set_opaque method

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(util/sexpr/options): add is_eqp predicate for options

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(kernel/type_checker): use expression before normalization in the unification constraints generated by the typechecker

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
refactor(kernel): add unfold_opaque flag to normalizer, modify how type checker uses the opaque flag, remove hidden_defs, and mark most builtin definitions as opaque

After this commit, in the type checker, when checking convertability, we first compute a normal form without expanding opaque terms.
If the terms are convertible, then we are done, and saved a lot of time by not expanding unnecessary definitions.
If they are not, instead of throwing an error, we try again expanding the opaque terms.
This seems to be the best of both worlds.
The opaque flag is a hint for the type checker, but it would never prevent us from type checking  a valid term.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
fix(library/fo_unify): bug at function that extracts the lhs and rhs of homogeneous/heterogeneous equality

For homogeneous equality, arg #1 is the Type of the lhs/rhs.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
fix(library/tactic/apply_tactic): provide the metavar_env to instantiate, the goal is to avoid add_lift and add_inst local entries

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
refactor(kernel/instantiate): remove hackish (dead) function

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(frontends/lean/parser): include proof state in exception for tactic failure

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(frontends/lean): improve error messages when elaborator cannot instantiate all metavariables

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