mathlib docs: core.init.meta.expr

source

structure pos :

Type

line : ℕ
column : ℕ

Column and line position in a Lean source file.

source

@[instance]

def pos.decidable_eq :

decidable_eq pos

Equations

pos.decidable_eq {line := l₁, column := c₁} {line := l₂, column := c₂} = dite (l₁ = l₂) (λ (h₁ : l₁ = l₂), dite (c₁ = c₂) (λ (h₂ : c₁ = c₂), decidable.is_true _) (λ (h₂ : ¬c₁ = c₂), decidable.is_false _)) (λ (h₁ : ¬l₁ = l₂), decidable.is_false _)

source

@[instance]

meta def pos.has_to_format :

has_to_format pos

source

inductive binder_info :

Type

default : binder_info
implicit : binder_info
strict_implicit : binder_info
inst_implicit : binder_info
aux_decl : 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 : ℕ⦄, ℕ

source

@[instance]

def binder_info.has_repr :

has_repr binder_info

Equations

binder_info.has_repr = {repr := λ (bi : binder_info), binder_info.has_repr._match_1 bi}
binder_info.has_repr._match_1 binder_info.aux_decl = "aux_decl"
binder_info.has_repr._match_1 binder_info.inst_implicit = "inst_implicit"
binder_info.has_repr._match_1 binder_info.strict_implicit = "strict_implicit"
binder_info.has_repr._match_1 binder_info.implicit = "implicit"
binder_info.has_repr._match_1 binder_info.default = "default"

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: lean meta def Y : (α → α) → α | f := f (Y f) The Y that appears in f (Y f) is a macro.
Builtin projections: lean 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 :

(bool := bool.tt) → Type

var : Π (elaborated : bool := bool.tt), ℕ → expr elaborated
sort : Π (elaborated : bool := bool.tt), level → expr elaborated
const : Π (elaborated : bool := bool.tt), name → list level → expr elaborated
mvar : Π (elaborated : bool := bool.tt), name → name → expr elaborated → expr elaborated
local_const : Π (elaborated : bool := bool.tt), name → name → binder_info → expr elaborated → expr elaborated
app : Π (elaborated : bool := bool.tt), expr elaborated → expr elaborated → expr elaborated
lam : Π (elaborated : bool := bool.tt), name → binder_info → expr elaborated → expr elaborated → expr elaborated
pi : Π (elaborated : bool := bool.tt), name → binder_info → expr elaborated → expr elaborated → expr elaborated
elet : Π (elaborated : bool := bool.tt), name → expr elaborated → expr elaborated → expr elaborated → expr elaborated
macro : Π (elaborated : bool := bool.tt), macro_def → list (expr elaborated) → expr elaborated

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.

source

@[instance]

meta def expr.inhabited :

inhabited expr

source

meta constant expr.macro_def_name :

macro_def → name

Get the name of the macro definition.

source

meta def expr.mk_var :

ℕ → 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 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

meta constant expr.to_string {elab : bool} :

expr elab → string

source

@[instance]

meta def expr.has_to_string {elab : bool} :

has_to_string (expr elab)

source

@[instance]

meta def expr.has_to_format {elab : bool} :

has_to_format (expr elab)

source

@[instance]

meta def expr.has_coe_to_fun {elab : bool} :

has_coe_to_fun (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

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

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]

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

source

meta def reflected.to_expr {α : Sort u} {a : α} :

reflected a → expr

source