mathlib documentation

core / init.meta.expr

structure pos  :
Type

Column and line position in a Lean source file.

@[protected, instance]
Equations
@[protected, instance]
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 : ℕ⦄, ℕ
@[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 := 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.

@[protected, instance]
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]

Compares expressions, including binder names.

meta constant expr.alpha_eqv  :
exprexprbool

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  :
expr

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  :
exprexprbool

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

meta constant expr.lex_lt  :
exprexprbool

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(exproption expr)expr

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  :
exprnameexpr

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  :
exprlist nameexpr

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  :
exprexprexpr

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

meta constant expr.instantiate_univ_params  :

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  :
exprexprexpr

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  :
exprexprexpr

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

meta constant expr.instantiate_vars  :
exprlist exprexpr

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

meta constant expr.instantiate_vars_core  :
exprlist exprexpr

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  :
expr

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  :
exprbool

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  :
exprexpr

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  :
exprexpr

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 elaboption pos

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

meta constant expr.copy_pos_info  :
exprexprexpr

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  :
exprexprbool

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  :

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

meta constant expr.get_weight  :
expr

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

meta constant expr.get_depth  :
expr

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

meta constant expr.mk_delayed_abstraction  :
exprlist nameexpr

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]
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.

Instances
meta def reflected.to_expr {α : Sort u} {a : α} :
meta def reflected.subst {α : Sort v} {β : α → Sort u} {f : Π (a : α), β a} {a : α} :
reflected freflected areflected (f a)
@[protected, instance]
meta constant expr.reflect {elab : bool} (e : expr elab) :
@[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 : reflected a] :
@[protected, instance]
meta def reflected.has_to_format {α : Sort u_1} (a : α) :
meta def expr.lt_prop (a b : expr) :
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 (name × expr)) (e : expr) :
meta def expr.is_var  :
meta def expr.app_of_list  :
exprlist exprexpr
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.mk_app  :
exprlist exprexpr
meta def expr.mk_binding (ctor : namebinder_infoexprexprexpr) (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  :
exprexpr
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 elabnamebool
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_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.

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  :
exprexpr

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  :
expr
meta def expr.lam_arity  :
expr
meta def expr.imp (a b : expr) :
meta def expr.lambdas  :
list exprexprexpr

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

meta def expr.pis  :
list exprexprexpr

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.

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} :
meta def expr_set  :
Type
meta def mk_expr_set  :