Skip to content

Metaprogramming for dummies

Jump to bottom
Moritz Doll edited this page May 25, 2023 · 23 revisions

Metaprogramming reference guide

This is an overview to the most common functions that are useful for writing tactics in Lean 4. We assume some knowledge of functional programming and a basic understanding of how metaprogramming works in Lean 4. The standard references are Lean 4 Metaprogramming book and Functional Programming in Lean, respectively.

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
  • Expr.getAppFnArgs: This is useful if you have an expression and you want to pattern-match

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)

However, see also: Qq.

Macros

Antiquotations

  • The easy stuff
  • Qq (Qq is love, Qq is life).

If you want to build expressions, it's a good idea to use Qq instead of manually building them from the constructors. The Q(α) macro is a synonym of Expr, with the (unchecked?) assertion that any e : Q(α) typechecks to have type α. And you can build elements of Q using q, and it will automatically, statically, fill in implicits. Instances are looked up in the context of the q invocation.

Unfortunately, errors generated by Qq are hard to understand.

Debugging

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

initialize registerTraceClass `identifier

Clone this wiki locally