implementation of tactic mode?

Stream: lean4

[Siddhartha Gadgil]

My motivation is to try to call tactics from within code. Is it correct that the block starting with a by is converted by a macro from TacticM Unit to the expected type? If so where is the macro?

Thanks.

[Leonardo de Moura]

We have different syntax categories in Lean. The main ones are: command, term, and tactic.
The term category contains the parser "by " tacticSeq : term where tacticSeq is roughly a sequence of tactics.
The parser produces objects of type Syntax.
The three main syntactic categories are processed using the following extensible functions.

elabCommand (stx : Syntax) : CommandElabM Unit
elabTerm (stx : Syntax) (expectedType? : Option Expr)  : TermElabM Expr
evalTactic (stx : Syntax) : TacticM Unit

All of them expand macros which are functions from Syntax to MacroM Syntax.
The evalTactic is essentially an interpreter.
We say it is extensible because users can add new functions for handling the new syntax they have defined. Mathlib4 contains many extensions already
https://github.com/leanprover-community/mathlib4/blob/master/Mathlib/Tactic/Basic.lean
The elab command used in this file is a macro that allows users to define new syntax and the "eval" function for the syntax in a single command.

[Siddhartha Gadgil]

Thank you very much.