feat(frontends/lean/scanner): use Lua style comments in Lean

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(frontends/lean): use '(* ... *)' instead of '(** ... **)' for script code blocks

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(frontends/lean/parser): combine Echo and Show commands into the 'print' command

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(builtin/macros): rename 'For' macro to 'take'

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(frontends/lean/parser): rename 'show' expression to 'have'

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(frontends/lean): use lowercase commands, replace 'endscope' and 'endnamespace' with 'end'

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(doc/lean): include lean documentation scripts in the test set

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
fix(frontends/lean): must invoke lua GC before closing a scope, reason: we may still have references to the current environment inside of the Lua state object

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(*): change name conventions for Lean builtin libraries

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(builtin/kernel): use the same notation for mp, eq::mp and forall::elim

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

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
chore(frontends/lean): rename setoption and setopaque commands to set::option and set::opaque

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(frontends/lean): add 'using' command

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
fix(builtin/Nat): name convention

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