Metaprogramming for dummies

Metaprogramming reference guide

Monads

Important metaprogramming monads

• MetaM is the monad you want to use if you modify metavariables.

• TacticM is the topmost monad for tactic-writing. You can get and set goals, etc

Going up

In a do block (←) takes care of bumping to a stronger monad

General monadology

• mapM
• (←)
• filterM

Objects

Expressions

Syntax

• elabTerm
• elabTermForApply
• elabTermEnsuringType

LocalDecl

withLocalDeclD

LocalContext

Names

Expressions

open Lean.Expr

Metavariables

Check whether something is a metavariable: isMVar Create metavariable: Assign metavariable: Check whether it is assigned

Note about delayed assignments (and reference to meta-book)

Free variables

isFVar fvarId! FVarId.getUserName

Bounded variables

isBVar

Lambdas

isLambda lambdaTelescope

Foralls

isForall forallTelescope

Applications

isApp getAppFn getAppNumArgs getAppArgs

The rest

Goals

open Lean.Elab.Tactic

getGoals getMainGoal setGoals

Tactics

open Lean.Elab.Tactic

evalTactic withMainContext liftMetaTactic

Lean.MVarId.apply

Example: If no universe levels: mvarId.apply (mkConst foo []) If known universe levels: mvarId.apply (mkConst foo [u,v]) Otherwise: mvarId.apply (← mkConstWithFreshMVarLevels ``foo)

Macros

Antiquotations

• The easy stuff
• Qq

Debugging

• dbg_trace "foo {var}" -- Very lowlevel works everywhere
• logInfo "foo" -- works in any monad that supports logging
• trace[identifier] "foo"

initialize registerTraceClass `identifier