core / init.meta.expr_address

inductive expr.coord :

Type

app_fn : expr.coord
app_arg : expr.coord
lam_var_type : expr.coord
lam_body : expr.coord
pi_var_type : expr.coord
pi_body : expr.coord
elet_var_type : expr.coord
elet_assignment : expr.coord
elet_body : expr.coord

An enum representing a recursive argument in an expr constructor. Types of local and meta variables are not included because they are not consistently set and depend on context.

source

def expr.coord.code :

expr.coord → ℕ

Convert the coord enum to its index number.

Equations

source

@[protected]

def expr.coord.repr :

expr.coord → string

Equations

expr.coord.elet_body.repr = "elet_body"
expr.coord.elet_assignment.repr = "elet_assignment"
expr.coord.elet_var_type.repr = "elet_var_type"
expr.coord.pi_body.repr = "pi_body"
expr.coord.pi_var_type.repr = "pi_var_type"
expr.coord.lam_body.repr = "lam_body"
expr.coord.lam_var_type.repr = "lam_var_type"
expr.coord.app_arg.repr = "app_arg"
expr.coord.app_fn.repr = "app_fn"

source

@[protected, instance]

def expr.coord.has_repr :

has_repr expr.coord

Equations

expr.coord.has_repr = {repr := expr.coord.repr}

source

@[protected, instance]

def expr.coord.has_to_string :

has_to_string expr.coord

Equations

expr.coord.has_to_string = {to_string := expr.coord.repr}

source

@[protected, instance]

meta def expr.coord.has_to_format :

has_to_format expr.coord

source

@[protected, instance]

meta def expr.coord.has_dec_eq :

decidable_eq expr.coord

source

@[protected, instance]

def expr.coord.has_lt :

has_lt expr.coord

Equations

expr.coord.has_lt = {lt := λ (x y : expr.coord), x.code < y.code}

source

meta def expr.coord.follow :

expr.coord → expr → option expr

Use this to pick the subexpression of a given expression that cooresponds to the given coordinate.

source

def expr.address :

Type

An address is a list of coordinates used to reference subterms of an expression. The first coordinate in the list corresponds to the root of the expression.

Equations