mathlib documentation

core / init.meta.environment

meta constant environment :

Type

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

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

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)

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

meta structure environment.intro_rule :

Type

constr : name
type : expr
infer : environment.implicit_infer_kind

One introduction rule in an inductive declaration

meta constant environment.mk_std :

ℕ → environment

Create a standard environment using the given trust level

meta constant environment.trust_lvl :

environment → ℕ

Return the trust level of the given environment

meta constant environment.add :

environment → declaration → exceptional environment

Add a new declaration to the environment

meta constant environment.mk_protected :

environment → name → environment

make declaration n protected

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

exceptional environment

add declaration d and make it protected

meta constant environment.is_protected :

environment → name → bool

check if n is the name of a protected declaration

meta constant environment.get :

environment → name → exceptional declaration

Retrieve a declaration from the environment

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

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

exceptional environment

meta constant environment.add_namespace :

environment → name → environment

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

meta constant environment.mark_namespace_as_open :

environment → name → environment

Mark a namespace as open

meta constant environment.execute_open :

environment → name → environment

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

meta constant environment.get_namespaces :

environment → list name

Retrieve all registered namespaces

meta constant environment.is_namespace :

environment → name → bool

Return tt iff the given name is a namespace

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

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

meta constant environment.is_inductive :

environment → name → bool

Return tt iff the given name is an inductive datatype

meta constant environment.is_constructor :

environment → name → bool

Return tt iff the given name is a constructor

meta constant environment.is_recursor :

environment → name → bool

Return tt iff the given name is a recursor

meta constant environment.is_recursive :

environment → name → bool

Return tt iff the given name is a recursive inductive datatype

meta constant environment.inductive_type_of :

environment → name → option name

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

meta constant environment.constructors_of :

environment → name → list name

Return the constructors of the inductive datatype with the given name

meta constant environment.recursor_of :

environment → name → option name

Return the recursor of the given inductive datatype

meta constant environment.inductive_num_params :

environment → name → ℕ

Return the number of parameters of the inductive datatype

meta constant environment.inductive_num_indices :

environment → name → ℕ

Return the number of indices of the inductive datatype

meta constant environment.inductive_dep_elim :

environment → name → bool

Return tt iff the inductive datatype recursor supports dependent elimination

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.

meta constant environment.is_projection :

environment → name → option environment.projection_info

See the docstring for projection_info.

meta constant environment.fold {α : Type} :

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

Fold over declarations in the environment.

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.

meta constant environment.refl_for :

environment → name → option name

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

meta constant environment.symm_for :

environment → name → option name

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

meta constant environment.trans_for :

environment → name → option name

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

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.

meta constant environment.decl_pos :

environment → name → option pos

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

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.

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

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]

meta constant environment.fingerprint :

environment → ℕ

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

meta constant environment.get_eqn_lemmas_for (env : environment) (n : name) :

Gets the equation lemmas for the declaration n.

meta constant environment.get_ext_eqn_lemmas_for (env : environment) (n : name) :

Gets the equation lemmas for the declaration n, including lemmas for match statements, etc.

meta constant environment.add_eqn_lemma (env : environment) (n : name) :

Adds the equation lemma n. It is added for the declaration t.pi_codomain.get_app_fn.const_name where t is the type of the equation lemma.

meta constant environment.unfold_untrusted_macros :

environment → expr → expr

meta constant environment.unfold_all_macros :

environment → expr → expr

meta def environment.is_constructor_app (env : environment) (e : expr) :

meta def environment.is_refl_app (env : environment) (e : expr) :

option (name × expr × expr)

meta def environment.in_current_file (env : environment) (n : name) :

Return true if 'n' has been declared in the current file

meta def environment.is_definition (env : environment) (n : name) :

@[protected, instance]

meta def environment.has_repr :

has_repr environment

@[protected, instance]

meta def environment.inhabited :

inhabited environment