MetaM
The Lean 4 metaprogramming API is organised around a small zoo of monads. The four main ones are:
CoreM
gives access to the environment, i.e. the set of things that have been declared or imported at the current point in the program.MetaM
gives access to the metavariable context, i.e. the set of metavariables that are currently declared and the values assigned to them (if any).TermElabM
gives access to various information used during elaboration.TacticM
gives access to the list of current goals.
These monads extend each other, so a MetaM
operation also has access to the
environment and a TermElabM
computation can use metavariables. There are also
other monads which do not neatly fit into this hierarchy, e.g. CommandElabM
extends MetaM
but neither extends nor is extended by TermElabM
.
This chapter demonstrates a number of useful operations in the MetaM
monad.
MetaM
is of particular importance because it allows us to give meaning to
every expression: the environment (from CoreM
) gives meaning to constants like
Nat.zero
or List.map
and the metavariable context gives meaning to both
metavariables and local hypotheses.
import Lean
open Lean Lean.Expr Lean.Meta
Metavariables
Overview
The 'Meta' in MetaM
refers to metavariables, so we should talk about these
first. Lean users do not usually interact much with metavariables  at least
not consciously  but they are used all over the place in metaprograms. There
are two ways to view them: as holes in an expression or as goals.
Take the goal perspective first. When we prove things in Lean, we always operate on goals, such as
n m : Nat
⊢ n + m = m + n
These goals are internally represented by metavariables. Accordingly, each
metavariable has a local context containing hypotheses (here [n : Nat, m : Nat]
) and a target type (here n + m = m + n
). Metavariables also have a
unique name, say m
, and we usually render them as ?m
.
To close a goal, we must give an expression e
of the target type. The
expression may contain fvars from the metavariable's local context, but no
others. Internally, closing a goal in this way corresponds to assigning the
metavariable; we write ?m := e
for this assignment.
The second, complementary view of metavariables is that they represent holes
in an expression. For instance, an application of Eq.trans
may generate two
goals which look like this:
n m : Nat
⊢ n = ?x
n m : Nat
⊢ ?x = m
Here ?x
is another metavariable  a hole in the target types of both goals,
to be filled in later during the proof. The type of ?x
is Nat
and its local
context is [n : Nat, m : Nat]
. Now, if we solve the first goal by reflexivity,
then ?x
must be n
, so we assign ?x := n
. Crucially, this also affects the
second goal: it is "updated" (not really, as we will see) to have target n = m
. The metavariable ?x
represents the same expression everywhere it occurs.
Tactic Communication via Metavariables
Tactics use metavariables to communicate the current goals. To see how, consider this simple (and slightly artificial) proof:
example {α} (a : α) (f : α → α) (h : ∀ a, f a = a) : f (f a) = a := by
apply Eq.trans
apply h
apply h
After we enter tactic mode, our ultimate goal is to generate an expression of
type f (f a) = a
which may involve the hypotheses α
, a
, f
and h
. So
Lean generates a metavariable ?m1
with target f (f a) = a
and a local
context containing these hypotheses. This metavariable is passed to the first
apply
tactic as the current goal.
The apply
tactic then tries to apply Eq.trans
and succeeds, generating three
new metavariables:
...
⊢ f (f a) = ?b
...
⊢ ?b = a
...
⊢ α
Call these metavariables ?m2
, ?m3
and ?b
. The last one, ?b
, stands for
the intermediate element of the transitivity proof and occurs in ?m2
and
?m3
. The local contexts of all metavariables in this proof are the same, so
we omit them.
Having created these metavariables, apply
assigns
?m1 := @Eq.trans α (f (f a)) ?b a ?m2 ?m3
and reports that ?m2
, ?m3
and ?b
are now the current goals.
At this point the second apply
tactic takes over. It receives ?m2
as the
current goal and applies h
to it. This succeeds and the tactic assigns ?m2 := h (f a)
. This assignment implies that ?b
must be f a
, so the tactic also
assigns ?b := f a
. Assigned metavariables are not considered open goals, so
the only goal that remains is ?m3
.
Now the third apply
comes in. Since ?b
has been assigned, the target of
?m3
is now f a = a
. Again, the application of h
succeeds and the
tactic assigns ?m3 := h a
.
At this point, all metavariables are assigned as follows:
?m1 := @Eq.trans α (f (f a)) ?b a ?m2 ?m3
?m2 := h (f a)
?m3 := h a
?b := f a
Exiting the by
block, Lean constructs the final proof term by taking the
assignment of ?m1
and replacing each metavariable with its assignment. This
yields
@Eq.trans α (f (f a)) (f a) a (h (f a)) (h a)
The example also shows how the two views of metavariables  as holes in an expression or as goals  are related: the goals we get are holes in the final proof term.
Basic Operations
Let us make these concepts concrete. When we operate in the MetaM
monad, we
have readwrite access to a MetavarContext
structure containing information
about the currently declared metavariables. Each metavariable is identified by
an MVarId
(a unique Name
). To create a new metavariable, we use
Lean.Meta.mkFreshExprMVar
with type
mkFreshExprMVar (type? : Option Expr) (kind := MetavarKind.natural)
(userName := Name.anonymous) : MetaM Expr
Its arguments are:
type?
: the target type of the new metavariable. Ifnone
, the target type isSort ?u
, where?u
is a universe level metavariable. (This is a special class of metavariables for universe levels, distinct from the expression metavariables which we have been calling simply "metavariables".)kind
: the metavariable kind. See the Metavariable Kinds section (but the default is usually correct).userName
: the new metavariable's userfacing name. This is what gets printed when the metavariable appears in a goal. Unlike theMVarId
, this name does not need to be unique.
The returned Expr
is always a metavariable. We can use Lean.Expr.mvarId!
to
extract the MVarId
, which is guaranteed to be unique. (Arguably
mkFreshExprMVar
should just return the MVarId
.)
The local context of the new metavariable is inherited from the current local
context, more about which in the next section. If you want to give a different
local context, use Lean.Meta.mkFreshExprMVarAt
.
Metavariables are initially unassigned. To assign them, use
Lean.MVarId.assign
with type
assign (mvarId : MVarId) (val : Expr) : MetaM Unit
This updates the MetavarContext
with the assignment ?mvarId := val
. You must
make sure that mvarId
is not assigned yet (or that the old assignment is
definitionally equal to the new assignment). You must also make sure that the
assigned value, val
, has the right type. This means (a) that val
must have
the target type of mvarId
and (b) that val
must only contain fvars from the
local context of mvarId
.
If you #check Lean.MVarId.assign
, you will see that its real type is more
general than the one we showed above: it works in any monad that has access to a
MetavarContext
. But MetaM
is by far the most important such monad, so in
this chapter, we specialise the types of assign
and similar functions.
To get information about a declared metavariable, use Lean.MVarId.getDecl
.
Given an MVarId
, this returns a MetavarDecl
structure. (If no metavariable
with the given MVarId
is declared, the function throws an exception.) The
MetavarDecl
contains information about the metavariable, e.g. its type, local
context and userfacing name. This function has some convenient variants, such
as Lean.MVarId.getType
.
To get the current assignment of a metavariable (if any), use
Lean.getExprMVarAssignment?
. To check whether a metavariable is assigned, use
Lean.MVarId.isAssigned
. However, these functions are relatively rarely
used in tactic code because we usually prefer a more powerful operation:
Lean.Meta.instantiateMVars
with type
instantiateMVars : Expr → MetaM Expr
Given an expression e
, instantiateMVars
replaces any assigned metavariable
?m
in e
with its assigned value. Unassigned metavariables remain as they
are.
This operation should be used liberally. When we assign a metavariable, existing
expressions containing this metavariable are not immediately updated. This is a
problem when, for example, we match on an expression to check whether it is an
equation. Without instantiateMVars
, we might miss the fact that the expression
?m
, where ?m
happens to be assigned to 0 = n
, represents an equation. In
other words, instantiateMVars
brings our expressions up to date with the
current metavariable state.
Instantiating metavariables requires a full traversal of the input expression,
so it can be somewhat expensive. But if the input expression does not contain
any metavariables, instantiateMVars
is essentially free. Since this is the
common case, liberal use of instantiateMVars
is fine in most situations.
Before we go on, here is a synthetic example demonstrating how the basic metavariable operations are used. More natural examples appear in the following sections.
#eval show MetaM Unit from do
 Create two fresh metavariables of type `Nat`.
let mvar1 ← mkFreshExprMVar (Expr.const ``Nat []) (userName := `mvar1)
let mvar2 ← mkFreshExprMVar (Expr.const ``Nat []) (userName := `mvar2)
 Create a fresh metavariable of type `Nat → Nat`. The `mkArrow` function
 creates a function type.
let mvar3 ← mkFreshExprMVar (← mkArrow (.const ``Nat []) (.const ``Nat []))
(userName := `mvar3)
 Define a helper function that prints each metavariable.
let printMVars : MetaM Unit := do
IO.println s!" meta1: {← instantiateMVars mvar1}"
IO.println s!" meta2: {← instantiateMVars mvar2}"
IO.println s!" meta3: {← instantiateMVars mvar3}"
IO.println "Initially, all metavariables are unassigned:"
printMVars
 Assign `mvar1 : Nat := ?mvar3 ?mvar2`.
mvar1.mvarId!.assign (.app mvar3 mvar2)
IO.println "After assigning mvar1:"
printMVars
 Assign `mvar2 : Nat := 0`.
mvar2.mvarId!.assign (.const ``Nat.zero [])
IO.println "After assigning mvar2:"
printMVars
 Assign `mvar3 : Nat → Nat := Nat.succ`.
mvar3.mvarId!.assign (.const ``Nat.succ [])
IO.println "After assigning mvar3:"
printMVars
 Initially, all metavariables are unassigned:
 meta1: ?_uniq.1
 meta2: ?_uniq.2
 meta3: ?_uniq.3
 After assigning mvar1:
 meta1: ?_uniq.3 ?_uniq.2
 meta2: ?_uniq.2
 meta3: ?_uniq.3
 After assigning mvar2:
 meta1: ?_uniq.3 Nat.zero
 meta2: Nat.zero
 meta3: ?_uniq.3
 After assigning mvar3:
 meta1: Nat.succ Nat.zero
 meta2: Nat.zero
 meta3: Nat.succ
Local Contexts
Consider the expression e
which refers to the free variable with unique name
h
:
e := .fvar (FVarId.mk `h)
What is the type of this expression? The answer depends on the local context in
which e
is interpreted. One local context may declare that h
is a local
hypothesis of type Nat
; another local context may declare that h
is a local
definition with value List.map
.
Thus, expressions are only meaningful if they are interpreted in the local
context for which they were intended. And as we saw, each metavariable has its
own local context. So in principle, functions which manipulate expressions
should have an additional MVarId
argument specifying the goal in which the
expression should be interpreted.
That would be cumbersome, so Lean goes a slightly different route. In MetaM
,
we always have access to an ambient LocalContext
, obtained with Lean.getLCtx
of type
getLCtx : MetaM LocalContext
All operations involving fvars use this ambient local context.
The downside of this setup is that we always need to update the ambient local
context to match the goal we are currently working on. To do this, we use
Lean.MVarId.withContext
of type
withContext (mvarId : MVarId) (c : MetaM α) : MetaM α
This function takes a metavariable mvarId
and a MetaM
computation c
and
executes c
with the ambient context set to the local context of mvarId
. A
typical use case looks like this:
def someTactic (mvarId : MVarId) ... : ... :=
mvarId.withContext do
...
The tactic receives the current goal as the metavariable mvarId
and
immediately sets the current local context. Any operations within the do
block
then use the local context of mvarId
.
Once we have the local context properly set, we can manipulate fvars. Like
metavariables, fvars are identified by an FVarId
(a unique Name
). Basic
operations include:
Lean.FVarId.getDecl : FVarId → MetaM LocalDecl
retrieves the declaration of a local hypothesis. As with metavariables, aLocalDecl
contains all information pertaining to the local hypothesis, e.g. its type and its userfacing name.Lean.Meta.getLocalDeclFromUserName : Name → MetaM LocalDecl
retrieves the declaration of the local hypothesis with the given userfacing name. If there are multiple such hypotheses, the bottommost one is returned. If there is none, an exception is thrown.
We can also iterate over all hypotheses in the local context, using the ForIn
instance of LocalContext
. A typical pattern is this:
for ldecl in ← getLCtx do
if ldecl.isImplementationDetail then
continue
 do something with the ldecl
The loop iterates over every LocalDecl
in the context. The
isImplementationDetail
check skips local hypotheses which are 'implementation
details', meaning they are introduced by Lean or by tactics for bookkeeping
purposes. They are not shown to users and tactics are expected to ignore them.
At this point, we can build the MetaM
part of an assumption
tactic:
def myAssumption (mvarId : MVarId) : MetaM Bool := do
 Check that `mvarId` is not already assigned.
mvarId.checkNotAssigned `myAssumption
 Use the local context of `mvarId`.
mvarId.withContext do
 The target is the type of `mvarId`.
let target ← mvarId.getType
 For each hypothesis in the local context:
for ldecl in ← getLCtx do
 If the hypothesis is an implementation detail, skip it.
if ldecl.isImplementationDetail then
continue
 If the type of the hypothesis is definitionally equal to the target
 type:
if ← isDefEq ldecl.type target then
 Use the local hypothesis to prove the goal.
mvarId.assign ldecl.toExpr
 Stop and return true.
return true
 If we have not found any suitable local hypothesis, return false.
return false
The myAssumption
tactic contains three functions we have not seen before:
Lean.MVarId.checkNotAssigned
checks that a metavariable is not already assigned. The 'myAssumption' argument is the name of the current tactic. It is used to generate a nicer error message.Lean.Meta.isDefEq
checks whether two definitions are definitionally equal. See the Definitional Equality section.Lean.LocalDecl.toExpr
is a helper function which constructs thefvar
expression corresponding to a local hypothesis.
Delayed Assignments
The above discussion of metavariable assignment contains a lie by omission: there are actually two ways to assign a metavariable. We have seen the regular way; the other way is called a delayed assignment.
We do not discuss delayed assignments in any detail here since they are rarely
useful for tactic writing. If you want to learn more about them, see the
comments in MetavarContext.lean
in the Lean standard library. But they create
two complications which you should be aware of.
First, delayed assignments make Lean.MVarId.isAssigned
and
getExprMVarAssignment?
mediumcalibre footguns. These functions only check for
regular assignments, so you may need to use Lean.MVarId.isDelayedAssigned
and Lean.Meta.getDelayedMVarAssignment?
as well.
Second, delayed assignments break an intuitive invariant. You may have assumed
that any metavariable which remains in the output of instantiateMVars
is
unassigned, since the assigned metavariables have been substituted. But delayed
metavariables can only be substituted once their assigned value contains no
unassigned metavariables. So delayedassigned metavariables can appear in an
expression even after instantiateMVars
.
Metavariable Depth
Metavariable depth is also a niche feature, but one that is occasionally useful.
Any metavariable has a depth (a natural number), and a MetavarContext
has a
corresponding depth as well. Lean only assigns a metavariable if its depth is
equal to the depth of the current MetavarContext
. Newly created metavariables
inherit the MetavarContext
's depth, so by default every metavariable is
assignable.
This setup can be used when a tactic needs some temporary metavariables and also needs to make sure that other, nontemporary metavariables will not be assigned. To ensure this, the tactic proceeds as follows:
 Save the current
MetavarContext
.  Increase the depth of the
MetavarContext
.  Perform whatever computation is necessary, possibly creating and assigning
metavariables. Newly created metavariables are at the current depth of the
MetavarContext
and so can be assigned. Old metavariables are at a lower depth, so cannot be assigned.  Restore the saved
MetavarContext
, thereby erasing all the temporary metavariables and resetting theMetavarContext
depth.
This pattern is encapsulated in Lean.Meta.withNewMCtxDepth
.
Computation
Computation is a core concept of dependent type theory. The terms 2
, Nat.succ 1
and 1 + 1
are all "the same" in the sense that they compute the same value.
We call them definitionally equal. The problem with this, from a
metaprogramming perspective, is that definitionally equal terms may be
represented by entirely different expressions, but our users would usually
expect that a tactic which works for 2
also works for 1 + 1
. So when we
write our tactics, we must do additional work to ensure that definitionally
equal terms are treated similarly.
Full Normalisation
The simplest thing we can do with computation is to bring a term into normal
form. With some exceptions for numeric types, the normal form of a term t
of
type T
is a sequence of applications of T
's constructors. E.g. the normal
form of a list is a sequence of applications of List.cons
and List.nil
.
The function that normalises a term (i.e. brings it into normal form) is
Lean.Meta.reduce
with type signature
reduce (e : Expr) (explicitOnly skipTypes skipProofs := true) : MetaM Expr
We can use it like this:
def someNumber : Nat := (· + 2) $ 3
#eval Expr.const ``someNumber []
 Lean.Expr.const `someNumber []
#eval reduce (Expr.const ``someNumber [])
 Lean.Expr.lit (Lean.Literal.natVal 5)
Incidentally, this shows that the normal form of a term of type Nat
is not
always an application of the constructors of Nat
; it can also be a literal.
Also note that #eval
can be used not only to evaluate a term, but also to
execute a MetaM
program.
The optional arguments of reduce
allow us to skip certain parts of an
expression. E.g. reduce e (explicitOnly := true)
does not normalise any
implicit arguments in the expression e
. This yields better performance: since
normal forms can be very big, it may be a good idea to skip parts of an
expression that the user is not going to see anyway.
The #reduce
command is essentially an application of reduce
:
#reduce someNumber
 5
Transparency
An ugly but important detail of Lean 4 metaprogramming is that any given expression does not have a single normal form. Rather, it has a normal form up to a given transparency.
A transparency is a value of Lean.Meta.TransparencyMode
, an enumeration with
four values: reducible
, instances
, default
and all
. Any MetaM
computation has access to an ambient TransparencyMode
which can be obtained
with Lean.Meta.getTransparency
.
The current transparency determines which constants get unfolded during
normalisation, e.g. by reduce
. (To unfold a constant means to replace it with
its definition.) The four settings unfold progressively more constants:
reducible
: unfold only constants tagged with the@[reducible]
attribute. Note thatabbrev
is a shorthand for@[reducible] def
.instances
: unfold reducible constants and constants tagged with the@[instance]
attribute. Again, theinstance
command is a shorthand for@[instance] def
.default
: unfold all constants except those tagged as@[irreducible]
.all
: unfold all constants, even those tagged as@[irreducible]
.
The ambient transparency is usually default
. To execute an operation with a
specific transparency, use Lean.Meta.withTransparency
. There are also
shorthands for specific transparencies, e.g. Lean.Meta.withReducible
.
Putting everything together for an example (where we use Lean.Meta.ppExpr
to
prettyprint an expression):
def traceConstWithTransparency (md : TransparencyMode) (c : Name) :
MetaM Format := do
ppExpr (← withTransparency md $ reduce (.const c []))
@[irreducible] def irreducibleDef : Nat := 1
def defaultDef : Nat := irreducibleDef + 1
abbrev reducibleDef : Nat := defaultDef + 1
We start with reducible
transparency, which only unfolds reducibleDef
:
#eval traceConstWithTransparency .reducible ``reducibleDef
 defaultDef + 1
If we repeat the above command but let Lean print implicit arguments as well,
we can see that the +
notation amounts to an application of the hAdd
function, which is a member of the HAdd
typeclass:
set_option pp.explicit true
#eval traceConstWithTransparency .reducible ``reducibleDef
 @HAdd.hAdd Nat Nat Nat (@instHAdd Nat instAddNat) defaultDef 1
When we reduce with instances
transparency, this applications is unfolded and
replaced by Nat.add
:
#eval traceConstWithTransparency .instances ``reducibleDef
 Nat.add defaultDef 1
With default
transparency, Nat.add
is unfolded as well:
#eval traceConstWithTransparency .default ``reducibleDef
 Nat.succ (Nat.succ irreducibleDef)
And with TransparencyMode.all
, we're finally able to unfold irreducibleDef
:
#eval traceConstWithTransparency .all ``reducibleDef
 3
The #eval
commands illustrate that the same term, reducibleDef
, can have a
different normal form for each transparency.
Why all this ceremony? Essentially for performance: if we allowed normalisation to always unfold every constant, operations such as type class search would become prohibitively expensive. The tradeoff is that we must choose the appropriate transparency for each operation that involves normalisation.
Weak Head Normalisation
Transparency addresses some of the performance issues with normalisation. But
even more important is to recognise that for many purposes, we don't need to
fully normalise terms at all. Suppose we are building a tactic that
automatically splits hypotheses of the type P ∧ Q
. We might want this tactic
to recognise a hypothesis h : X
if X
reduces to P ∧ Q
. But if P
additionally reduces to Y ∨ Z
, the specific Y
and Z
do not concern us.
Reducing P
would be unnecessary work.
This situation is so common that the fully normalising reduce
is in fact
rarely used. Instead, the normalisation workhorse of Lean is whnf
, which
reduces an expression to weak head normal form (WHNF).
Roughly speaking, an expression e
is in weakhead normal form when it has the
form
e = f x₁ ... xₙ (n ≥ 0)
and f
cannot be reduced (at the current transparency). To conveniently check
the WHNF of an expression, we define a function whnf'
, using some functions
that will be discussed in the Elaboration chapter.
open Lean.Elab.Term in
def whnf' (e : TermElabM Syntax) : TermElabM Format := do
let e ← elabTermAndSynthesize (← e) none
ppExpr (← whnf e)
Now, here are some examples of expressions in WHNF.
Constructor applications are in WHNF (with some exceptions for numeric types):
#eval whnf' `(List.cons 1 [])
 [1]
The arguments of an application in WHNF may or may not be in WHNF themselves:
#eval whnf' `(List.cons (1 + 1) [])
 [1 + 1]
Applications of constants are in WHNF if the current transparency does not allow us to unfold the constants:
#eval withTransparency .reducible $ whnf' `(List.append [1] [2])
 List.append [1] [2]
Lambdas are in WHNF:
#eval whnf' `(λ x : Nat => x)
 fun x => x
Foralls are in WHNF:
#eval whnf' `(∀ x, x > 0)
 ∀ (x : Nat), x > 0
Sorts are in WHNF:
#eval whnf' `(Type 3)
 Type 3
Literals are in WHNF:
#eval whnf' `((15 : Nat))
 15
Here are some more expressions in WHNF which are a bit tricky to test:
?x 0 1  Assuming the metavariable `?x` is unassigned, it is in WHNF.
h 0 1  Assuming `h` is a local hypothesis, it is in WHNF.
On the flipside, here are some expressions that are not in WHNF.
Applications of constants are not in WHNF if the current transparency allows us to unfold the constants:
#eval whnf' `(List.append [1])
 fun x => 1 :: List.append [] x
Applications of lambdas are not in WHNF:
#eval whnf' `((λ x y : Nat => x + y) 1)
 `fun y => 1 + y`
let
bindings are not in WHNF:
#eval whnf' `(let x : Nat := 1; x)
 1
And again some tricky examples:
?x 0 1  Assuming `?x` is assigned (e.g. to `Nat.add`), its application is not
in WHNF.
h 0 1  Assuming `h` is a local definition (e.g. with value `Nat.add`), its
application is not in WHNF.
Returning to the tactic that motivated this section, let us write a function
that matches a type of the form P ∧ Q
, avoiding extra computation. WHNF
makes it easy:
def matchAndReducing (e : Expr) : MetaM (Option (Expr × Expr)) := do
match ← whnf e with
 (.app (.app (.const ``And _) P) Q) => return some (P, Q)
 _ => return none
By using whnf
, we ensure that if e
evaluates to something of the form P ∧ Q
, we'll notice. But at the same time, we don't perform any unnecessary
computation in P
or Q
.
However, our 'no unnecessary computation' mantra also means that if we want to
perform deeper matching on an expression, we need to use whnf
multiple times.
Suppose we want to match a type of the form P ∧ Q ∧ R
. The correct way to do
this uses whnf
twice:
def matchAndReducing₂ (e : Expr) : MetaM (Option (Expr × Expr × Expr)) := do
match ← whnf e with
 (.app (.app (.const ``And _) P) e') =>
match ← whnf e' with
 (.app (.app (.const ``And _) Q) R) => return some (P, Q, R)
 _ => return none
 _ => return none
This sort of deep matching up to computation could be automated. But until
someone builds this automation, we have to figure out the necessary whnf
s
ourselves.
Definitional Equality
As mentioned, definitional equality is equality up to computation. Two
expressions t
and s
are definitionally equal or defeq (at the current
transparency) if their normal forms (at the current transparency) are equal.
To check whether two expressions are defeq, use Lean.Meta.isDefEq
with type
signature
isDefEq : Expr → Expr → MetaM Bool
Even though definitional equality is defined in terms of normal forms, isDefEq
does not actually compute the normal forms of its arguments, which would be very
expensive. Instead, it tries to "match up" t
and s
using as few reductions
as possible. This is a necessarily heuristic endeavour and when the heuristics
misfire, isDefEq
can become very expensive. In the worst case, it may have to
reduce s
and t
so often that they end up in normal form anyway. But usually
the heuristics are good and isDefEq
is reasonably fast.
If expressions t
and u
contain assignable metavariables, isDefEq
may
assign these metavariables to make t
defeq to u
. We also say that isDefEq
unifies t
and u
; such unification queries are sometimes written t =?= u
.
For instance, the unification List ?m =?= List Nat
succeeds and assigns ?m := Nat
. The unification Nat.succ ?m =?= n + 1
succeeds and assigns ?m := n
.
The unification ?m₁ + ?m₂ + ?m₃ =?= m + n  k
fails and no metavariables are
assigned (even though there is a 'partial match' between the expressions).
Whether isDefEq
considers a metavariable assignable is determined by two
factors:
 The metavariable's depth must be equal to the current
MetavarContext
depth. See the Metavariable Depth section.  Each metavariable has a kind (a value of type
MetavarKind
) whose sole purpose is to modify the behaviour ofisDefEq
. Possible kinds are: Natural:
isDefEq
may freely assign the metavariable. This is the default.  Synthetic:
isDefEq
may assign the metavariable, but avoids doing so if possible. For example, suppose?n
is a natural metavariable and?s
is a synthetic metavariable. When faced with the unification problem?s =?= ?n
,isDefEq
assigns?n
rather than?s
.  Synthetic opaque:
isDefEq
never assigns the metavariable.
 Natural:
Constructing Expressions
In the previous chapter, we saw some primitive functions for building
expressions: Expr.app
, Expr.const
, mkAppN
and so on. There is nothing
wrong with these functions, but the additional facilities of MetaM
often
provide more convenient ways.
Applications
When we write regular Lean code, Lean helpfully infers many implicit arguments and universe levels. If it did not, our code would look rather ugly:
def appendAppend (xs ys : List α) := (xs.append ys).append xs
set_option pp.all true in
set_option pp.explicit true in
#print appendAppend
 def appendAppend.{u_1} : {α : Type u_1} → List.{u_1} α → List.{u_1} α → List.{u_1} α :=
 fun {α : Type u_1} (xs ys : List.{u_1} α) => @List.append.{u_1} α (@List.append.{u_1} α xs ys) xs
The .{u_1}
suffixes are universe levels, which must be given for every
polymorphic constant. And of course the type α
is passed around everywhere.
Exactly the same problem occurs during metaprogramming when we construct expressions. A handmade expression representing the righthand side of the above definition looks like this:
def appendAppendRHSExpr₁ (u : Level) (α xs ys : Expr) : Expr :=
mkAppN (.const ``List.append [u])
#[α, mkAppN (.const ``List.append [u]) #[α, xs, ys], xs]
Having to specify the implicit arguments and universe levels is annoying and
errorprone. So MetaM
provides a helper function which allows us to omit
implicit information: Lean.Meta.mkAppM
of type
mkAppM : Name → Array Expr → MetaM Expr
Like mkAppN
, mkAppM
constructs an application. But while mkAppN
requires
us to give all universe levels and implicit arguments ourselves, mkAppM
infers
them. This means we only need to provide the explicit arguments, which makes for
a much shorter example:
def appendAppendRHSExpr₂ (xs ys : Expr) : MetaM Expr := do
mkAppM ``List.append #[← mkAppM ``List.append #[xs, ys], xs]
Note the absence of any α
s and u
s. There is also a variant of mkAppM
,
mkAppM'
, which takes an Expr
instead of a Name
as the first argument,
allowing us to construct applications of expressions which are not constants.
However, mkAppM
is not magic: if you write mkAppM ``List.append #[]
, you
will get an error at runtime. This is because mkAppM
tries to determine what
the type α
is, but with no arguments given to append
, α
could be anything,
so mkAppM
fails.
Another occasionally useful variant of mkAppM
is Lean.Meta.mkAppOptM
of type
mkAppOptM : Name → Array (Option Expr) → MetaM Expr
Whereas mkAppM
always infers implicit and instance arguments and always
requires us to give explicit arguments, mkAppOptM
lets us choose freely which
arguments to provide and which to infer. With this, we can, for example, give
instances explicitly, which we use in the following example to give a
nonstandard Ord
instance.
def revOrd : Ord Nat where
compare x y := compare y x
def ordExpr : MetaM Expr := do
mkAppOptM ``compare #[none, Expr.const ``revOrd [], mkNatLit 0, mkNatLit 1]
#eval format <$> ordExpr
 Ord.compare.{0} Nat revOrd
 (OfNat.ofNat.{0} Nat 0 (instOfNatNat 0))
 (OfNat.ofNat.{0} Nat 1 (instOfNatNat 1))
Like mkAppM
, mkAppOptM
has a primed variant Lean.Meta.mkAppOptM'
which
takes an Expr
instead of a Name
as the first argument. The file which
contains mkAppM
also contains various other helper functions, e.g. for making
list literals or sorry
s.
Lambdas and Foralls
Another common task is to construct expressions involving λ
or ∀
binders.
Suppose we want to create the expression λ (x : Nat), Nat.add x x
. One way is
to write out the lambda directly:
def doubleExpr₁ : Expr :=
.lam `x (.const ``Nat []) (mkAppN (.const ``Nat.add []) #[.bvar 0, .bvar 0])
BinderInfo.default
#eval ppExpr doubleExpr₁
 fun x => Nat.add x x
This works, but the use of bvar
is highly unidiomatic. Lean uses a socalled
locally closed variable representation. This means that all but the
lowestlevel functions in the Lean API expect expressions not to contain 'loose
bvar
s', where a bvar
is loose if it is not bound by a binder in the same
expression. (Outside of Lean, such variables are usually called 'free'. The name
bvar
 'bound variable'  already indicates that bvar
s are never supposed
to be free.)
As a result, if in the above example we replace mkAppN
with the slightly
higherlevel mkAppM
, we get a runtime error. Adhering to the locally closed
convention, mkAppM
expects any expressions given to it to have no loose bound
variables, and .bvar 0
is precisely that.
So instead of using bvar
s directly, the Lean way is to construct expressions
with bound variables in two steps:
 Construct the body of the expression (in our example: the body of the
lambda), using temporary local hypotheses (
fvar
s) to stand in for the bound variables.  Replace these
fvar
s withbvar
s and, at the same time, add the corresponding lambda binders.
This process ensures that we do not need to handle expressions with loose
bvar
s at any point (except during step 2, which is performed 'atomically' by a
bespoke function). Applying the process to our example:
def doubleExpr₂ : MetaM Expr :=
withLocalDecl `x BinderInfo.default (.const ``Nat []) λ x => do
let body ← mkAppM ``Nat.add #[x, x]
mkLambdaFVars #[x] body
#eval show MetaM _ from do
ppExpr (← doubleExpr₂)
 fun x => Nat.add x x
There are two new functions. First, Lean.Meta.withLocalDecl
has type
withLocalDecl (name : Name) (bi : BinderInfo) (type : Expr) (k : Expr → MetaM α) : MetaM α
Given a variable name, binder info and type, withLocalDecl
constructs a new
fvar
and passes it to the computation k
. The fvar
is available in the local
context during the execution of k
but is deleted again afterwards.
The second new function is Lean.Meta.mkLambdaFVars
with type (ignoring some
optional arguments)
mkLambdaFVars : Array Expr → Expr → MetaM Expr
This function takes an array of fvar
s and an expression e
. It then adds one
lambda binder for each fvar
x
and replaces every occurrence of x
in e
with a bound variable corresponding to the new lambda binder. The returned
expression does not contain the fvar
s any more, which is good since they
disappear after we leave the withLocalDecl
context. (Instead of fvar
s, we
can also give mvar
s to mkLambdaFVars
, despite its name.)
Some variants of the above functions may be useful:
withLocalDecls
declares multiple temporaryfvar
s.mkForallFVars
creates∀
binders instead ofλ
binders.mkLetFVars
createslet
binders.mkArrow
is the nondependent version ofmkForallFVars
which construcs a function typeX → Y
. Since the type is nondependent, there is no need for temporaryfvar
s.
Using all these functions, we can construct larger expressions such as this one:
λ (f : Nat → Nat), ∀ (n : Nat), f n = f (n + 1)
def somePropExpr : MetaM Expr := do
let funcType ← mkArrow (.const ``Nat []) (.const ``Nat [])
withLocalDecl `f BinderInfo.default funcType fun f => do
let feqn ← withLocalDecl `n BinderInfo.default (.const ``Nat []) fun n => do
let lhs := .app f n
let rhs := .app f (← mkAppM ``Nat.succ #[n])
let eqn ← mkEq lhs rhs
mkForallFVars #[n] eqn
mkLambdaFVars #[f] feqn
The next line registers someProp
as a name for the expression we've just
constructed, allowing us to play with it more easily. The mechanisms behind this
are discussed in the Elaboration chapter.
elab "someProp" : term => somePropExpr
#check someProp
 fun f => ∀ (n : Nat), f n = f (Nat.succ n) : (Nat → Nat) → Prop
#reduce someProp Nat.succ
 ∀ (n : Nat), Nat.succ n = Nat.succ (Nat.succ n)
Deconstructing Expressions
Just like we can construct expressions more easily in MetaM
, we can also
deconstruct them more easily. Particularly useful is a family of functions for
deconstructing expressions which start with λ
and ∀
binders.
When we are given a type of the form ∀ (x₁ : T₁) ... (xₙ : Tₙ), U
, we are
often interested in doing something with the conclusion U
. For instance, the
apply
tactic, when given an expression e : ∀ ..., U
, compares U
with the
current target to determine whether e
can be applied.
To do this, we could repeatedly match on the type expression, removing ∀
binders until we get to U
. But this would leave us with an U
containing
unbound bvar
s, which, as we saw, is bad. Instead, we use
Lean.Meta.forallTelescope
of type
forallTelescope (type : Expr) (k : Array Expr → Expr → MetaM α) : MetaM α
Given type = ∀ (x₁ : T₁) ... (xₙ : Tₙ), U x₁ ... xₙ
, this function creates one
fvar fᵢ
for each ∀
bound variable xᵢ
and replaces each xᵢ
with fᵢ
in
the conclusion U
. It then calls the computation k
, passing it the fᵢ
and
the conclusion U f₁ ... fₙ
. Within this computation, the fᵢ
are registered
in the local context; afterwards, they are deleted again (similar to
withLocalDecl
).
There are many useful variants of forallTelescope
:
forallTelescopeReducing
: likeforallTelescope
but matching is performed up to computation. This means that if you have an expressionX
which is different from but defeq to∀ x, P x
,forallTelescopeReducing X
will deconstructX
intox
andP x
. The nonreducingforallTelescope
would not recogniseX
as a quantified expression. The matching is performed by essentially callingwhnf
repeatedly, using the ambient transparency.forallBoundedTelescope
: likeforallTelescopeReducing
(even though there is no "reducing" in the name) but stops after a specified number of∀
binders.forallMetaTelescope
,forallMetaTelescopeReducing
,forallMetaBoundedTelescope
: like the corresponding nonmeta
functions, but the bound variables are replaced by newmvar
s instead offvar
s. Unlike the nonmeta
functions, themeta
functions do not delete the new metavariables after performing some computation, so the metavariables remain in the environment indefinitely.lambdaTelescope
,lambdaTelescopeReducing
,lambdaBoundedTelescope
,lambdaMetaTelescope
: like the correspondingforall
functions, but forλ
binders instead of∀
.
Using one of the telescope functions, we can implement our own apply
tactic:
def myApply (goal : MVarId) (e : Expr) : MetaM (List MVarId) := do
 Check that the goal is not yet assigned.
goal.checkNotAssigned `myApply
 Operate in the local context of the goal.
goal.withContext do
 Get the goal's target type.
let target ← goal.getType
 Get the type of the given expression.
let type ← inferType e
 If `type` has the form `∀ (x₁ : T₁) ... (xₙ : Tₙ), U`, introduce new
 metavariables for the `xᵢ` and obtain the conclusion `U`. (If `type` does
 not have this form, `args` is empty and `conclusion = type`.)
let (args, _, conclusion) ← forallMetaTelescopeReducing type
 If the conclusion unifies with the target:
if ← isDefEq target conclusion then
 Assign the goal to `e x₁ ... xₙ`, where the `xᵢ` are the fresh
 metavariables in `args`.
goal.assign (mkAppN e args)
 `isDefEq` may have assigned some of the `args`. Report the rest as new
 goals.
let newGoals ← args.filterMapM λ mvar => do
let mvarId := mvar.mvarId!
if ! (← mvarId.isAssigned) && ! (← mvarId.isDelayedAssigned) then
return some mvarId
else
return none
return newGoals.toList
 If the conclusion does not unify with the target, throw an error.
else
throwTacticEx `myApply goal m!"{e} is not applicable to goal with target {target}"
The real apply
does some additional pre and postprocessing, but the core
logic is what we show here. To test our tactic, we need an elaboration
incantation, more about which in the Elaboration chapter.
elab "myApply" e:term : tactic => do
let e ← Elab.Term.elabTerm e none
Elab.Tactic.liftMetaTactic (myApply · e)
example (h : α → β) (a : α) : β := by
myApply h
myApply a
Backtracking
Many tactics naturally require backtracking: the ability to go back to a previous state, as if the tactic had never been executed. A few examples:
first  t  u
first executest
. Ift
fails, it backtracks and executesu
.try t
executest
. Ift
fails, it backtracks to the initial state, erasing any changes made byt
.trivial
attempts to solve the goal using a number of simple tactics (e.g.rfl
orcontradiction
). After each unsuccessful application of such a tactic,trivial
backtracks.
Good thing, then, that Lean's core data structures are designed to enable easy
and efficient backtracking. The corresponding API is provided by the
Lean.MonadBacktrack
class. MetaM
, TermElabM
and TacticM
are all
instances of this class. (CoreM
is not but could be.)
MonadBacktrack
provides two fundamental operations:
Lean.saveState : m s
returns a representation of the current state, wherem
is the monad we are in ands
is the state type. E.g. forMetaM
,saveState
returns aLean.Meta.SavedState
containing the current environment, the currentMetavarContext
and various other pieces of information.Lean.restoreState : s → m Unit
takes a previously saved state and restores it. This effectively resets the compiler state to the previous point.
With this, we can roll our own MetaM
version of the try
tactic:
def tryM (x : MetaM Unit) : MetaM Unit := do
let s ← saveState
try
x
catch _ =>
restoreState s
We first save the state, then execute x
. If x
fails, we backtrack the state.
The standard library defines many combinators like tryM
. Here are the most
useful ones:
Lean.withoutModifyingState (x : m α) : m α
executes the actionx
, then resets the state and returnsx
's result. You can use this, for example, to check for definitional equality without assigning metavariables:
IfwithoutModifyingState $ isDefEq x y
isDefEq
succeeds, it may assign metavariables inx
andy
. UsingwithoutModifyingState
, we can make sure this does not happen.Lean.observing? (x : m α) : m (Option α)
executes the actionx
. Ifx
succeeds,observing?
returns its result. Ifx
fails (throws an exception),observing?
backtracks the state and returnsnone
. This is a more informative version of ourtryM
combinator.Lean.commitIfNoEx (x : α) : m α
executesx
. Ifx
succeeds,commitIfNoEx
returns its result. Ifx
throws an exception,commitIfNoEx
backtracks the state and rethrows the exception.
Note that the builtin try ... catch ... finally
does not perform any
backtracking. So code which looks like this is probably wrong:
try
doSomething
catch e =>
doSomethingElse
The catch
branch, doSomethingElse
, is executed in a state containing
whatever modifications doSomething
made before it failed. Since we probably
want to erase these modifications, we should write instead:
try
commitIfNoEx doSomething
catch e =>
doSomethingElse
Another MonadBacktrack
gotcha is that restoreState
does not backtrack the
entire state. Caches, trace messages and the global name generator, among
other things, are not backtracked, so changes made to these parts of the state
are not reset by restoreState
. This is usually what we want: if a tactic
executed by observing?
produces some trace messages, we want to see them even
if the tactic fails. See Lean.Meta.SavedState.restore
and Lean.Core.restore
for details on what is and is not backtracked.
In the next chapter, we move towards the topic of elaboration, of which you've already seen several glimpses in this chapter. We start by discussing Lean's syntax system, which allows you to add custom syntactic constructs to the Lean parser.
Exercises

[Metavariables] Create a metavariable with type
Nat
, and assign to it value3
. Notice that changing the type of the metavariable fromNat
to, for example,String
, doesn't raise any errors  that's why, as was mentioned, we must make sure "(a) thatval
must have the target type ofmvarId
and (b) thatval
must only containfvars
from the local context ofmvarId
". 
[Metavariables] What would
instantiateMVars (Lean.mkAppN (Expr.const 'Nat.add []) #[mkNatLit 1, mkNatLit 2])
output? 
[Metavariables] Fill in the missing lines in the following code.
#eval show MetaM Unit from do let oneExpr := Expr.app (Expr.const `Nat.succ []) (Expr.const ``Nat.zero []) let twoExpr := Expr.app (Expr.const `Nat.succ []) oneExpr  Create `mvar1` with type `Nat`  let mvar1 ← ...  Create `mvar2` with type `Nat`  let mvar2 ← ...  Create `mvar3` with type `Nat`  let mvar3 ← ...  Assign `mvar1` to `2 + ?mvar2 + ?mvar3`  ...  Assign `mvar3` to `1`  ...  Instantiate `mvar1`, which should result in expression `2 + ?mvar2 + 1` ...

[Metavariables] Consider the theorem
red
, and tacticexplore
below. a) What would be thetype
anduserName
of metavariablemvarId
? b) What would be thetype
s anduserName
s of all local declarations in this metavariable's local context? Print them all out.elab "explore" : tactic => do let mvarId : MVarId ← Lean.Elab.Tactic.getMainGoal let metavarDecl : MetavarDecl ← mvarId.getDecl IO.println "Our metavariable"  ... IO.println "All of its local declarations"  ... theorem red (hA : 1 = 1) (hB : 2 = 2) : 2 = 2 := by explore sorry

[Metavariables] Write a tactic
solve
that proves the theoremred
. 
[Computation] What is the normal form of the following expressions: a)
fun x => x
of typeBool → Bool
b)(fun x => x) ((true && false)  true)
of typeBool
c)800 + 2
of typeNat

[Computation] Show that
1
created withExpr.lit (Lean.Literal.natVal 1)
is definitionally equal to an expression created withExpr.app (Expr.const ``Nat.succ []) (Expr.const ``Nat.zero [])
. 
[Computation] Determine whether the following expressions are definitionally equal. If
Lean.Meta.isDefEq
succeeds, and it leads to metavariable assignment, write down the assignments. a)5 =?= (fun x => 5) ((fun y : Nat → Nat => y) (fun z : Nat => z))
b)2 + 1 =?= 1 + 2
c)?a =?= 2
, where?a
has a typeString
d)?a + Int =?= "hi" + ?b
, where?a
and?b
don't have a type e)2 + ?a =?= 3
f)2 + ?a =?= 2 + 1

[Computation] Write down what you expect the following code to output.
@[reducible] def reducibleDef : Nat := 1  same as `abbrev` @[instance] def instanceDef : Nat := 2  same as `instance` def defaultDef : Nat := 3 @[irreducible] def irreducibleDef : Nat := 4 @[reducible] def sum := [reducibleDef, instanceDef, defaultDef, irreducibleDef] #eval show MetaM Unit from do let constantExpr := Expr.const `sum [] Meta.withTransparency Meta.TransparencyMode.reducible do let reducedExpr ← Meta.reduce constantExpr dbg_trace (← ppExpr reducedExpr)  ... Meta.withTransparency Meta.TransparencyMode.instances do let reducedExpr ← Meta.reduce constantExpr dbg_trace (← ppExpr reducedExpr)  ... Meta.withTransparency Meta.TransparencyMode.default do let reducedExpr ← Meta.reduce constantExpr dbg_trace (← ppExpr reducedExpr)  ... Meta.withTransparency Meta.TransparencyMode.all do let reducedExpr ← Meta.reduce constantExpr dbg_trace (← ppExpr reducedExpr)  ... let reducedExpr ← Meta.reduce constantExpr dbg_trace (← ppExpr reducedExpr)  ...

[Constructing Expressions] Create expression
fun x, 1 + x
in two ways: a) not idiomatically, with loose bound variables b) idiomatically. In what version can you useLean.mkAppN
? In what version can you useLean.Meta.mkAppM
? 
[Constructing Expressions] Create expression
∀ (yellow: Nat), yellow
. 
[Constructing Expressions] Create expression
∀ (n : Nat), n = n + 1
in two ways: a) not idiomatically, with loose bound variables b) idiomatically. In what version can you useLean.mkApp3
? In what version can you useLean.Meta.mkEq
? 
[Constructing Expressions] Create expression
fun (f : Nat → Nat), ∀ (n : Nat), f n = f (n + 1)
idiomatically. 
[Constructing Expressions] What would you expect the output of the following code to be?
#eval show Lean.Elab.Term.TermElabM _ from do let stx : Syntax ← `(∀ (a : Prop) (b : Prop), a ∨ b → b → a ∧ a) let expr ← Elab.Term.elabTermAndSynthesize stx none let (_, _, conclusion) ← forallMetaTelescope expr dbg_trace conclusion  ... let (_, _, conclusion) ← forallMetaBoundedTelescope expr 2 dbg_trace conclusion  ... let (_, _, conclusion) ← lambdaMetaTelescope expr dbg_trace conclusion  ...

[Backtracking] Check that the expressions
?a + Int
and"hi" + ?b
are definitionally equal withisDefEq
(make sure to use the proper types orOption.none
for the types of your metavariables!). UsesaveState
andrestoreState
to revert metavariable assignments.