# mathlibdocumentation

core / init.meta.expr

structure pos  :
Type

Column and line position in a Lean source file.

Instances for pos
@[protected, instance]
Equations
@[protected, instance]
meta def pos.has_to_format  :
inductive binder_info  :
Type

Auxiliary annotation for binders (Lambda and Pi). This information is only used for elaboration. The difference between {} and ⦃⦄ is how implicit arguments are treated that are not followed by explicit arguments. {} arguments are applied eagerly, while ⦃⦄ arguments are left partially applied:

def foo {x : ℕ} : ℕ := x
def bar ⦃x : ℕ⦄ : ℕ := x
#check foo -- foo : ℕ
#check bar -- bar : Π ⦃x : ℕ⦄, ℕ

Instances for binder_info
@[protected, instance]
Equations
meta constant macro_def  :
Type

Macros are basically "promises" to build an expr by some C++ code, you can't build them in Lean. You can unfold a macro and force it to evaluate. They are used for

• sorry.
• Term placeholders (_) in pexprs.
• Expression annotations. See expr.is_annotation.
• Meta-recursive calls. Eg:
meta def Y : (α → α) → α | f := f (Y f)

The Y that appears in f (Y f) is a macro.
• Builtin projections:
structure foo := (mynat : ℕ)
#print foo.mynat
-- @[reducible]
-- def foo.mynat : foo → ℕ :=
-- λ (c : foo), [foo.mynat c]

The thing in square brackets is a macro.
• Ephemeral structures inside certain specialised C++ implemented tactics.
meta inductive expr (elaborated : bool := bool.tt) :
Type

An expression. eg (4+5).

The elab flag is indicates whether the expr has been elaborated and doesn't contain any placeholder macros. For example the equality x = x is represented in expr ff as app (app (const eq _) x) x while in expr tt it is represented as app (app (app (const eq _) t) x) x (one more argument). The VM replaces instances of this datatype with the C++ implementation.

Instances for expr
@[protected, instance]
meta def expr.inhabited {elab : bool} :
meta constant expr.macro_def_name (d : macro_def) :

Get the name of the macro definition.

meta def expr.mk_var (n : ) :
meta constant expr.is_annotation {elab : bool} :
expr elaboption (name × expr elab)

Expressions can be annotated using an annotation macro during compilation. For example, a have x:X, from p, q expression will be compiled to (λ x:X,q)(p), but nested in an annotation macro with the name "have". These annotations have no real semantic meaning, but are useful for helping Lean's pretty printer.

meta constant expr.is_string_macro {elab : bool} :
expr elaboption (expr elab)
meta def expr.erase_annotations {elab : bool} :
expr elabexpr elab

Remove all macro annotations from the given expr.

@[instance]
meta constant expr.has_decidable_eq  :

Compares expressions, including binder names.

meta constant expr.alpha_eqv  :
expr

Compares expressions while ignoring binder names.

@[protected]
meta constant expr.to_string {elab : bool} :
expr elabstring
@[protected, instance]
meta def expr.has_to_string {elab : bool} :
@[protected, instance]
meta def expr.has_to_format {elab : bool} :
@[protected, instance]
meta def expr.has_coe_to_fun {elab : bool} :
has_coe_to_fun (expr elab) (λ (e : expr elab), expr elabexpr elab)

Coercion for letting users write (f a) instead of (expr.app f a)

meta constant expr.hash  :

Each expression created by Lean carries a hash. This is calculated upon creation of the expression. Two structurally equal expressions will have the same hash.

meta constant expr.lt  :
expr

Compares expressions, ignoring binder names, and sorting by hash.

meta constant expr.lex_lt  :
expr

Compares expressions, ignoring binder names.

meta constant expr.fold {α : Type} :
exprα → (exprα → α) → α

expr.fold e a f: Traverses each subexpression of e. The nat passed to the folder f is the binder depth.

meta constant expr.replace  :
expr(exprexpr

expr.replace e f Traverse over an expr e with a function f which can decide to replace subexpressions or not. For each subexpression s in the expression tree, f s n is called where n is how many binders are present above the given subexpression s. If f s n returns none, the children of s will be traversed. Otherwise if some s' is returned, s' will replace s and this subexpression will not be traversed further.

meta constant expr.abstract_local  :
expr

abstract_local e n replaces each instance of the local constant with unique (not pretty) name n in e with a de-Bruijn variable.

meta constant expr.abstract_locals  :
expr

Multi version of abstract_local. Note that the given expression will only be traversed once, so this is not the same as list.foldl expr.abstract_local.

meta def expr.abstract  :
expr

abstract e x Abstracts the expression e over the local constant x.

meta constant expr.instantiate_univ_params  :
exprlist expr

Expressions depend on levels, and these may depend on universe parameters which have names. instantiate_univ_params e [(n₁,l₁), ...] will traverse e and replace any universe parameters with name nᵢ with the corresponding level lᵢ.

meta constant expr.instantiate_nth_var  :
expr

instantiate_nth_var n a b takes the nth de-Bruijn variable in a and replaces each occurrence with b.

meta constant expr.instantiate_var  :
expr

instantiate_var a b takes the 0th de-Bruijn variable in a and replaces each occurrence with b.

meta constant expr.instantiate_vars  :
expr

instantiate_vars (#0 #1 #2) [x,y,z] = (%%x %%y %%z)

meta constant expr.instantiate_vars_core  :
expr

Same as instantiate_vars except lifts and shifts the vars by the given amount. instantiate_vars_core (#0 #1 #2 #3) 0 [x,y] = (x y #0 #1) instantiate_vars_core (#0 #1 #2 #3) 1 [x,y] = (#0 x y #1) instantiate_vars_core (#0 #1 #2 #3) 2 [x,y] = (#0 #1 x y)

@[protected]
meta constant expr.subst {elab : bool} :
expr elabexpr elabexpr elab

Perform beta-reduction if the left expression is a lambda, or construct an application otherwise. That is: expr.subst (λ x, %%Y) Z = Y[x/Z], and expr.subst X Z = X.app Z otherwise

meta constant expr.get_free_var_range  :

get_free_var_range e returns one plus the maximum de-Bruijn value in e. Eg get_free_var_range(#1 #0)yields2

meta constant expr.has_var  :

has_var e returns true iff e has free variables.

meta constant expr.has_var_idx  :
expr

has_var_idx e n returns true iff e has a free variable with de-Bruijn index n.

meta constant expr.has_local  :

has_local e returns true if e contains a local constant.

meta constant expr.has_meta_var  :

has_meta_var e returns true iff e contains a metavariable.

meta constant expr.lower_vars  :
expr

lower_vars e s d lowers the free variables >= s in e by d. Note that this can cause variable clashes. examples:

• lower_vars (#2 #1 #0) 1 1 = (#1 #0 #0)
• lower_vars (λ x, #2 #1 #0) 1 1 = (λ x, #1 #1 #0 )
meta constant expr.lift_vars  :
expr

Lifts free variables. lift_vars e s d will lift all free variables with index ≥ s in e by d.

@[protected]
meta constant expr.pos {elab : bool} :
expr elab

Get the position of the given expression in the Lean source file, if anywhere.

meta constant expr.copy_pos_info  :
expr

copy_pos_info src tgt copies position information from src to tgt.

meta constant expr.is_internal_cnstr  :

Returns some n when the given expression is a constant with the name ..._cnstr.n

is_internal_cnstr : expr → option unsigned
|(const (mk_numeral n (mk_string "_cnstr" _)) _) := some n
|_ := none


[NOTE] This is not used anywhere in core Lean.

meta constant expr.get_nat_value  :

There is a macro called a "nat_value_macro" holding a natural number which are used during compilation. This function extracts that to a natural number. [NOTE] This is not used anywhere in Lean.

meta constant expr.collect_univ_params  :

Get a list of all of the universe parameters that the given expression depends on.

meta constant expr.occurs  :
expr

occurs e t returns tt iff e occurs in t up to α-equivalence. Purely structural: no unification or definitional equality.

meta constant expr.has_local_in  :
expr

Returns true if any of the names in the given name_set are present in the given expr.

meta constant expr.get_weight  :

Computes the number of sub-expressions (constant time).

meta constant expr.get_depth  :

Computes the maximum depth of the expression (constant time).

meta constant expr.mk_delayed_abstraction  :
expr

mk_delayed_abstraction m ls creates a delayed abstraction on the metavariable m with the unique names of the local constants ls. If m is not a metavariable then this is equivalent to abstract_locals.

If the given expression is a delayed abstraction macro, return some ls where ls is a list of unique names of locals that will be abstracted.

@[class, irreducible]
meta def reflected (α : Sort u) :
α → Type

(reflected a) is a special opaque container for a closed expr representing a. It can only be obtained via type class inference, which will use the representation of a in the calling context. Local constants in the representation are replaced by nested inference of reflected instances.

The quotation expression (a) (outside of patterns) is equivalent to reflect a and thus can be used as an explicit way of inferring an instance of reflected a.

Note that the α argument is explicit to prevent it being treated as reducible by typeclass inference, as this breaks reflected instances on type synonyms.

Instances of this typeclass
Instances of other typeclasses for reflected
@[irreducible]
meta def reflected.to_expr {α : Sort u} {a : α} :
aexpr
@[irreducible]
meta def reflected.subst {α : Sort v} {β : α → Sort u} {f : Π (a : α), β a} {a : α} :
reflected (Π (a : α), β a) f areflected (β a) (f a)

This is a more strongly-typed version of expr.subst that keeps track of the value being reflected. To obtain a term of type reflected _, use ((λ x y, foo x y).subst ex).subst ey instead of using (foo %%ex %%ey) (which returns an expr).

@[protected, instance]
meta constant expr.reflect {elab : bool} (e : expr elab) :
reflected (expr elab) e
@[protected, instance]
meta constant string.reflect (s : string) :
@[protected, instance]
meta def expr.has_coe {α : Sort u} (a : α) :
@[protected]
meta def reflect {α : Sort u} (a : α) [h : a] :
a
@[protected, instance]
meta def reflected.has_to_format {α : Sort u_1} (a : α) :
meta def expr.lt_prop (a b : expr) :
Prop
Instances for expr.lt_prop
@[protected, instance]
@[protected, instance]
meta def expr.has_lt  :

Compares expressions, ignoring binder names, and sorting by hash.

meta def expr.mk_true  :
meta def expr.mk_false  :
meta constant expr.mk_sorry (type : expr) :

Returns the sorry macro with the given type.

meta constant expr.is_sorry (e : expr) :

Checks whether e is sorry, and returns its type.

meta def expr.instantiate_local (n : name) (s e : expr) :

Replace each instance of the local constant with name n by the expression s in e.

meta def expr.instantiate_locals (s : list ) (e : expr) :
meta def expr.is_var  :
meta def expr.app_of_list  :
expr
meta def expr.is_app  :
meta def expr.app_fn  :
meta def expr.app_arg  :
meta def expr.get_app_fn {elab : bool} :
expr elabexpr elab
meta def expr.get_app_args_aux  :
meta def expr.get_app_args  :
meta def expr.mk_app  :
expr
meta def expr.mk_binding (ctor : namebinder_infoexpr) (e l : expr) :
meta def expr.bind_pi (e l : expr) :

(bind_pi e l) abstracts and pi-binds the local l in e

meta def expr.bind_lambda (e l : expr) :

(bind_lambda e l) abstracts and lambda-binds the local l in e

meta def expr.ith_arg_aux  :
expr
meta def expr.ith_arg (e : expr) (i : ) :
meta def expr.const_name {elab : bool} :
expr elabname
meta def expr.is_constant {elab : bool} :
expr elabbool
meta def expr.local_pp_name {elab : bool} :
expr elabname
meta def expr.local_type {elab : bool} :
expr elabexpr elab
meta def expr.is_aux_decl  :
meta def expr.is_constant_of {elab : bool} :
expr elab
meta def expr.is_app_of (e : expr) (n : name) :
meta def expr.is_napp_of (e : expr) (c : name) (n : ) :

The same as is_app_of but must also have exactly n arguments.

meta def expr.is_false  :
meta def expr.is_not  :
meta def expr.is_and  :
meta def expr.is_or  :
meta def expr.is_iff  :
meta def expr.is_eq  :
meta def expr.is_ne  :
meta def expr.is_bin_arith_app (e : expr) (op : name) :
meta def expr.is_lt (e : expr) :
meta def expr.is_gt (e : expr) :
meta def expr.is_le (e : expr) :
meta def expr.is_ge (e : expr) :
meta def expr.is_heq  :
meta def expr.is_lambda  :
meta def expr.is_pi  :
meta def expr.is_arrow  :
meta def expr.is_let  :
meta def expr.binding_name  :

The name of the bound variable in a pi, lambda or let expression.

meta def expr.binding_info  :

The binder info of a pi or lambda expression.

meta def expr.binding_domain  :

The domain (type of bound variable) of a pi, lambda or let expression.

meta def expr.binding_body  :

The body of a pi, lambda or let expression. This definition doesn't instantiate bound variables, and therefore produces a term that is open. See note [open expressions] in mathlib.

meta def expr.nth_binding_body  :

nth_binding_body n e iterates binding_body n times to an iterated pi expression e. This definition doesn't instantiate bound variables, and therefore produces a term that is open. See note [open expressions] in mathlib.

meta def expr.is_macro  :
meta def expr.is_numeral  :
meta def expr.pi_arity  :
meta def expr.lam_arity  :
meta def expr.imp (a b : expr) :
meta def expr.lambdas  :

lambdas cs e lambda binds e with each of the local constants in cs.

meta def expr.pis  :

Same as expr.lambdas but with pi.

meta def expr.to_raw_fmt {elab : bool} :
expr elabformat
meta def expr.mfold {α : Type} {m : Type → Type} [monad m] (e : expr) (a : α) (fn : exprα → m α) :
m α

Fold an accumulator a over each subexpression in the expression e. The nat passed to fn is the number of binders above the subexpression.

@[reducible]
meta def expr_map (data : Type) :
Type

An dictionary from data` to expressions.

meta def expr_map.mk (data : Type) :
meta def mk_expr_map {data : Type} :
@[reducible]
meta def expr_set  :
Type
meta def mk_expr_set  :