mathlib documentation

core / init.meta.expr

structure pos  :

Column and line position in a Lean source file.

Instances for pos
@[protected, instance]
Equations
@[protected, instance]
inductive binder_info  :

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  :

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

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 elab option (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 elab option (expr elab)
meta def expr.erase_annotations {elab : bool} :
expr elab expr elab

Remove all macro annotations from the given expr.

@[instance]

Compares expressions, including binder names.

meta constant expr.alpha_eqv  :

Compares expressions while ignoring binder names.

@[protected]
meta constant expr.to_string {elab : bool} :
@[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 elab expr 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  :

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

meta constant expr.lex_lt  :

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.

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  :

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

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.

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

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

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

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

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

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

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  :

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  :

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

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

meta constant expr.copy_pos_info  :

copy_pos_info src tgt copies position information from src to tgt.

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.

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

meta constant expr.occurs  :

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

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

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

(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 : α} :
@[irreducible]
meta def reflected.subst {α : Sort v} {β : α Sort u} {f : Π (a : α), β a} {a : α} :
reflected (Π (a : α), β a) f reflected α a reflected (β 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 : reflected α 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 (name × expr)) (e : expr) :
meta def expr.is_var  :
meta def expr.is_app  :
meta def expr.app_fn  :
meta def expr.get_app_fn {elab : bool} :
expr elab expr elab
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 (e : expr) (i : ) :
meta def expr.const_name {elab : bool} :
meta def expr.is_constant {elab : bool} :
meta def expr.local_pp_name {elab : bool} :
meta def expr.local_type {elab : bool} :
expr elab expr elab
meta def expr.is_constant_of {elab : bool} :
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_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_pi  :
meta def expr.is_let  :

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

The binder info of a pi or lambda expression.

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

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.

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.imp (a b : expr) :

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} :
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) :

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