feat(library/tactic): expose COND and WHEN tacticals in Lua, add HOL-like tactical names

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(library/tactic): expose conj_tactic, imp_tactic, conj_hyp_tactic in the Lua API

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(library/tactic): modify assumption_tactic, it should fail if not applicable, and TRY tactical

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
refactor(library/elaborator): simplify synthesizer interface

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(frontends/lean/parser): add basic tactic support in the frontend

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
fix(library/type_inferer): typo

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(frontends/lean/parse): allow script-code blocks to be used in the apply command

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
style(frontends/lean/parse): missing include

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
fix(tests/lua): incorrect assertion

The assertion got violated after a bug was fixed in the to_goal procedure.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(library/tactic): make THEN, ORELSE, APPEND, PAR and INTERLEAVE nary combinators

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(library/tactic): make THEN, ORELSE, APPEND, PAR and INTERLEAVE nary combinators