test(tests/lean/run): define below_rec_on (aka brec_on) for vectors
test(tests/lean/run): fibonacci using below_rec_on (aka brec_on)
feat(frontends/lean): add option pp.purify_metavars

It is true by default. If the user sets it to false, then
the internal metavariable names are used in the pretty printer
feat(frontends/lean): add elaborator.trace_instances option

When on this option allows us to visualize "class-instance resolution"
fix(frontends/lean): include position information
feat(frontends/lean): include file-name and line/col numbers when displaying class-instance resolution trace
feat(frontends/lean/placeholder_elaborator): add option 'elaborator.instance_max_depth'
feat(frontends/lean/placeholder_elaborator): include type in class-instance resolution trace
feat(frontends/lean/scanner): disallow hierarchical names such as 'x.1'
feat(frontends/lean): add variation of the foldl/foldr notation where initial element is suppressed, closes #314

See tests/lean/fold.lean for examples
fix(frontends/lean): tactic + variables bug, fixes #315
fix(frontends/lean): fix pretty-printing spacing problem
feat(frontends/lean/placeholder_elaborator): display instance trace header once per class-instance resolution problem
fix(library/definitional/no_confusion): assertion violation
feat(emacs/lean-syntax): highlight [decls] modifier
feat(frontends/lean): default 'eval' command ignores opaque/irreducible annotations

To retrieve the previous behavior, we should use [strict] modifier
test(tests/lean/run): fibonacci using well_founded recursion
refactor(library/data/nat/wf): mark theorem as transparent

It doesn't really help since
        le_imp_lt_or_eq, succ_le_cancel, lt_imp_le_succ and or.elim
are still opaque
feat(library/logic/wf): some basic definitions for constructing well_founded relations
fix(frontends/lean): coercion affects other modules