Tactics

A tactic is a term of type TacticM Unit. So it returns nothing. However, it changes the state of the system.

The todo tactic

The todo tactic is a simple tactic that logs a warning message with the string passed to it. It then replaces the main goal with a term built with sorry.

def tacticTodo_ : Lean.ParserDescr

Equations

• tacticTodo_ = Lean.ParserDescr.node `tacticTodo_ 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.nonReservedSymbol "todo" false) (Lean.ParserDescr.const `str))

def MyNames.myNat : Nat

Equations

• MyNames.myNat = 2

Metaprogramming in Lean

• A Lean program, term, command etc is given by a string.
• A parser converts this to syntax. A syntax can be of many types.
• The elaborator converts this to terms, commands or tactics in the internal foundations of lean.

def «command#stx[_]» : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def «command#expr[_]» : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def tacticScowl_ : Lean.ParserDescr

Equations

• tacticScowl_ = Lean.ParserDescr.node `tacticScowl_ 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.nonReservedSymbol "scowl" false) (Lean.ParserDescr.const `str))