core / init.meta.environment

source

meta constant environment :

Type

An environment contains all of the declarations and notation that have been defined so far.

Instances for environment

source

structure environment.projection_info :

Type

cname : name
nparams : ℕ
idx : ℕ
is_class : bool

Consider a type ψ which is an inductive datatype using a single constructor mk (a : α) (b : β) : ψ. Lean will automatically make two projection functions a : ψ → α, b : ψ → β. Lean tags these declarations as projections. This helps the simplifier / rewriter not have to expand projectors. Eg a (mk x y) will automatically reduce to x. If you extend a structure, all of the projections on the parent will also be created for the child. Projections are also treated differently in the VM for efficiency.

Note that projections have nothing to do with the dot mylist.map syntax.

You can find out if a declaration is a projection using environment.is_projection which returns projection_info.

Data for a projection declaration:

cname is the name of the constructor associated with the projection.
nparams is the number of constructor parameters. Eg and.intro has two type parameters.
idx is the parameter being projected by this projection.
is_class is tt iff this is a typeclass projection.

Examples: #

and.right is a projection with {cname := `and.intro, nparams := 2, idx := 1, is_class := ff}
ordered_ring.neg is a projection with {cname := `ordered_ring.mk, nparams := 1, idx := 5, is_class := tt}.

Instances for environment.projection_info

environment.projection_info.has_sizeof_inst
environment.projection_info.inhabited

source

inductive environment.implicit_infer_kind :

Type

implicit : environment.implicit_infer_kind
relaxed_implicit : environment.implicit_infer_kind
none : environment.implicit_infer_kind

A marking on the binders of structures and inductives indicating how this constructor should mark its parameters.

  inductive foo
  | one {} : foo -> foo   -- relaxed_implicit
  | two ( ) : foo -> foo  -- explicit
  | two [] : foo -> foo   -- implicit
  | three : foo -> foo    -- relaxed implicit (default)

Instances for environment.implicit_infer_kind

environment.implicit_infer_kind.has_sizeof_inst
environment.implicit_infer_kind.inhabited

source

@[protected, instance]

def environment.implicit_infer_kind.inhabited :

inhabited environment.implicit_infer_kind

Equations

environment.implicit_infer_kind.inhabited = {default := environment.implicit_infer_kind.implicit}

source

meta structure environment.intro_rule :

Type

constr : name
type : expr
infer : environment.implicit_infer_kind

One introduction rule in an inductive declaration

source

meta constant environment.mk_std :

ℕ → environment

Create a standard environment using the given trust level

source

meta constant environment.trust_lvl :

environment → ℕ

Return the trust level of the given environment

source

meta constant environment.add :

environment → declaration → exceptional environment

Add a new declaration to the environment

source

meta constant environment.mk_protected :

environment → name → environment

make declaration n protected

source

meta def environment.add_protected (env : environment) (d : declaration) :

exceptional environment

add declaration d and make it protected

source

meta constant environment.is_protected :

environment → name → bool

check if n is the name of a protected declaration

source

meta constant environment.get :

environment → name → exceptional declaration

Retrieve a declaration from the environment

source

meta def environment.contains (env : environment) (d : name) :

bool

source

meta constant environment.add_defn_eqns (env : environment) (opt : options) (lp_params : list name) (params : list expr) (sig : expr) (eqns : list (list (expr bool.ff) × expr)) (is_meta : bool) :

exceptional environment

source

meta constant environment.add_namespace :

environment → name → environment

Register the given name as a namespace, making it available to the open command

source

meta constant environment.mark_namespace_as_open :

environment → name → environment

Mark a namespace as open

source

meta constant environment.execute_open :

environment → name → environment

Modify the environment as if open %%name had been parsed

source

meta constant environment.get_namespaces :

environment → list name

Retrieve all registered namespaces

source

meta constant environment.is_namespace :

environment → name → bool

Return tt iff the given name is a namespace

source

meta constant environment.add_inductive (env : environment) (n : name) (levels : list name) (num_params : ℕ) (type : expr) (intros : list (name × expr)) (is_meta : bool) :

exceptional environment

Add a new inductive datatype to the environment name, universe parameters, number of parameters, type, constructors (name and type), is_meta

source

meta constant environment.add_ginductive (env : environment) (opt : options) (levels : list name) (params : list expr) (inds : list ((name × expr) × list environment.intro_rule)) (is_meta : bool) :

exceptional environment

Add a new general inductive declaration to the environment. This has the same effect as a inductive in the file, including generating all the auxiliary definitions, as well as triggering mutual/nested inductive compilation, by contrast to environment.add_inductive which only adds the core axioms supported by the kernel.

The inds argument should be a list of inductives in the mutual family. The first argument is a pair of the name of the type being constructed and the type of this inductive family (not including the params). The second argument is a list of intro rules, specified by a name, an implicit_infer_kind giving the implicitness of the params for this constructor, and an expression with the type of the constructor (not including the params).

source

meta constant environment.is_inductive :

environment → name → bool

Return tt iff the given name is an inductive datatype

source

meta constant environment.is_constructor :

environment → name → bool

Return tt iff the given name is a constructor

source

meta constant environment.is_recursor :

environment → name → bool

Return tt iff the given name is a recursor

source

meta constant environment.is_recursive :

environment → name → bool

Return tt iff the given name is a recursive inductive datatype

source

meta constant environment.inductive_type_of :

environment → name → option name

Return the name of the inductive datatype of the given constructor.

source

meta constant environment.constructors_of :

environment → name → list name

Return the constructors of the inductive datatype with the given name

source

meta constant environment.recursor_of :

environment → name → option name

Return the recursor of the given inductive datatype

source

meta constant environment.inductive_num_params :

environment → name → ℕ

Return the number of parameters of the inductive datatype

source

meta constant environment.inductive_num_indices :

environment → name → ℕ

Return the number of indices of the inductive datatype

source

meta constant environment.inductive_dep_elim :

environment → name → bool

Return tt iff the inductive datatype recursor supports dependent elimination

source

meta constant environment.is_ginductive :

environment → name → bool

Functionally equivalent to is_inductive.

Technically, this works by checking if the name is in the ginductive environment extension which is outside the kernel, whereas is_inductive works by looking at the kernel extension. But there are no is_inductives which are not is_ginductive.

source

meta constant environment.is_projection :

environment → name → option environment.projection_info

See the docstring for projection_info.

source

meta constant environment.fold {α : Type} :

environment → α → (declaration → α → α) → α

Fold over declarations in the environment.

source

meta constant environment.relation_info :

environment → name → option (ℕ × ℕ × ℕ)

relation_info env n returns some value if n is marked as a relation in the given environment. the tuple contains: total number of arguments of the relation, lhs position and rhs position.

source

meta constant environment.refl_for :

environment → name → option name

refl_for env R returns the name of the reflexivity theorem for the relation R

source

meta constant environment.symm_for :

environment → name → option name

symm_for env R returns the name of the symmetry theorem for the relation R

source

meta constant environment.trans_for :

environment → name → option name

trans_for env R returns the name of the transitivity theorem for the relation R

source

meta constant environment.decl_olean :

environment → name → option string

decl_olean env d returns the name of the .olean file where d was defined. The result is none if d was not defined in an imported file.

source

meta constant environment.decl_pos :

environment → name → option pos

decl_pos env d returns the source location of d if available.

source

meta constant environment.decl_noncomputable_reason :

environment → name → option name

decl_pos env d returns the name of a declaration that d inherits noncomputability from, or none if it is computable.

Note that this also returns none on axioms and constants. These can be detected by using environment.get_decl and declaration.is_axiom and declaration.is_constant.

source

meta constant environment.structure_fields :

environment → name → option (list name)

Return the fields of the structure with the given name, or none if it is not a structure

source

meta constant environment.get_class_attribute_symbols :

environment → name → name_set

get_class_attribute_symbols env attr_name return symbols occurring in instances of type classes tagged with the attribute attr_name. Example: [algebra]

source

meta constant environment.fingerprint :

environment → ℕ

The fingerprint of the environment is a hash formed from all of the declarations in the environment.

source