mathlib3 documentation

core / init.meta.expr

source
structure pos  :
Type

Column and line position in a Lean source file.

Instances for pos
source
@[protected, instance]
def pos.decidable_eq  :
decidable_eq pos
Equations
source
@[protected, instance]
meta def pos.has_to_format  :
has_to_format pos
source
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
source
@[protected, instance]
def binder_info.has_repr  :
has_repr binder_info
Equations
source
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.
source
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
source
@[protected, instance]
meta def expr.inhabited {elab : bool} :
inhabited (expr elab)
source
meta constant expr.macro_def_name (d : macro_def) :
name

Get the name of the macro definition.

source
meta def expr.mk_var (n : ℕ) :
expr
source
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.

source
meta constant expr.is_string_macro {elab : bool} :
expr elab → option (expr elab)
source
meta def expr.erase_annotations {elab : bool} :
expr elab → expr elab

Remove all macro annotations from the given expr.

source
@[instance]
meta constant expr.has_decidable_eq  :
decidable_eq expr

Compares expressions, including binder names.

source
meta constant expr.alpha_eqv  :
expr → expr → bool

Compares expressions while ignoring binder names.

source
@[protected]
meta constant expr.to_string {elab : bool} :
expr elab → string
source
@[protected, instance]
meta def expr.has_to_string {elab : bool} :
has_to_string (expr elab)
source
@[protected, instance]
meta def expr.has_to_format {elab : bool} :
has_to_format (expr elab)
source
@[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)

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

source
meta constant expr.lt  :
expr → expr → bool

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

source
meta constant expr.lex_lt  :
expr → expr → bool

Compares expressions, ignoring binder names.

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

source
meta constant expr.replace  :
expr → (expr → ℕ → option 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.

source
meta constant expr.abstract_local  :
expr → name → 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.

source
meta constant expr.abstract_locals  :
expr → list name → 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.

source
meta def expr.abstract  :
expr → expr → expr

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

source
meta constant expr.instantiate_univ_params  :
expr → list (name × level) → 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ᵢ.

source
meta constant expr.instantiate_nth_var  :
ℕ → expr → expr → expr

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

source
meta constant expr.instantiate_var  :
expr → expr → expr

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

source
meta constant expr.instantiate_vars  :
expr → list expr → expr

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

source
meta constant expr.instantiate_vars_core  :
expr → ℕ → list expr → 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)

source
@[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

source
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`

source
meta constant expr.has_var  :
expr → bool

has_var e returns true iff e has free variables.

source
meta constant expr.has_var_idx  :
expr → ℕ → bool

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

source
meta constant expr.has_local  :
expr → bool

has_local e returns true if e contains a local constant.

source
meta constant expr.has_meta_var  :
expr → bool

has_meta_var e returns true iff e contains a metavariable.

source
meta constant expr.lower_vars  :
expr → ℕ → ℕ → 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 )
source
meta constant expr.lift_vars  :
expr → ℕ → ℕ → expr

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

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

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

source
meta constant expr.copy_pos_info  :
expr → expr → expr

copy_pos_info src tgt copies position information from src to tgt.

source
meta constant expr.is_internal_cnstr  :
expr → option unsigned

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.

source
meta constant expr.get_nat_value  :
expr → option ℕ

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.

source
meta constant expr.collect_univ_params  :
expr → list name

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

source
meta constant expr.occurs  :
expr → expr → bool

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

source
meta constant expr.has_local_in  :
expr → name_set → bool

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

source
meta constant expr.get_weight  :
expr → ℕ

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

source
meta constant expr.get_depth  :
expr → ℕ

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

source
meta constant expr.mk_delayed_abstraction  :
expr → list name → 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.

source
meta constant expr.get_delayed_abstraction_locals  :
expr → option (list name)

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.

source
@[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
source
@[irreducible]
meta def reflected.to_expr {α : Sort u} {a : α} :
reflected α a → expr
source
@[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).

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

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

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

Returns the sorry macro with the given type.

source
meta constant expr.is_sorry (e : expr) :
option expr

Checks whether e is sorry, and returns its type.

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

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

source
meta def expr.instantiate_locals (s : list (name × expr)) (e : expr) :
expr
source
meta def expr.is_var  :
expr → bool
source
meta def expr.app_of_list  :
expr → list expr → expr
source
meta def expr.is_app  :
expr → bool
source
meta def expr.app_fn  :
expr → expr
source
meta def expr.app_arg  :
expr → expr
source
meta def expr.get_app_fn {elab : bool} :
expr elab → expr elab
source
meta def expr.get_app_num_args  :
expr → ℕ
source
meta def expr.get_app_args_aux  :
list expr → expr → list expr
source
meta def expr.get_app_args  :
expr → list expr
source
meta def expr.mk_app  :
expr → list expr → expr
source
meta def expr.mk_binding (ctor : name → binder_info → expr → expr → expr) (e l : expr) :
expr
source
meta def expr.bind_pi (e l : expr) :
expr

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

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

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

source
meta def expr.ith_arg_aux  :
expr → ℕ → expr
source
meta def expr.ith_arg (e : expr) (i : ℕ) :
expr
source
meta def expr.const_name {elab : bool} :
expr elab → name
source
meta def expr.is_constant {elab : bool} :
expr elab → bool
source
meta def expr.is_local_constant  :
expr → bool
source
meta def expr.local_uniq_name  :
expr → name
source
meta def expr.local_pp_name {elab : bool} :
expr elab → name
source
meta def expr.local_type {elab : bool} :
expr elab → expr elab
source
meta def expr.is_aux_decl  :
expr → bool
source
meta def expr.is_constant_of {elab : bool} :
expr elab → name → bool
source
meta def expr.is_app_of (e : expr) (n : name) :
bool
source
meta def expr.is_napp_of (e : expr) (c : name) (n : ℕ) :
bool

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

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

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

source
meta def expr.binding_info  :
expr → binder_info

The binder info of a pi or lambda expression.

source
meta def expr.binding_domain  :
expr → expr

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

source
meta def expr.binding_body  :
expr → expr

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.

source
meta def expr.nth_binding_body  :
ℕ → expr → expr

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.

source
meta def expr.is_macro  :
expr → bool
source
meta def expr.is_numeral  :
expr → bool
source
meta def expr.pi_arity  :
expr → ℕ
source
meta def expr.lam_arity  :
expr → ℕ
source
meta def expr.imp (a b : expr) :
expr
source
meta def expr.lambdas  :
list expr → expr → expr

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

source
meta def expr.pis  :
list expr → expr → expr

Same as expr.lambdas but with pi.

source
meta def expr.extract_opt_auto_param  :
expr → expr
source
meta def expr.to_raw_fmt {elab : bool} :
expr elab → format
source
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.

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

An dictionary from data to expressions.

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