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

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

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)
meta structure environment.intro_rule  :
Type

One introduction rule in an inductive declaration

meta constant environment.mk_std  :

Create a standard environment using the given trust level

meta constant environment.trust_lvl  :

Return the trust level of the given environment

Add a new declaration to the environment

make declaration n protected

add declaration d and make it protected

meta constant environment.is_protected  :

check if n is the name of a protected declaration

Retrieve a declaration from the environment

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

meta constant environment.is_namespace  :

Return tt iff the given name is a namespace

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

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  :

Return tt iff the given name is an inductive datatype

meta constant environment.is_constructor  :

Return tt iff the given name is a constructor

meta constant environment.is_recursor  :

Return tt iff the given name is a recursor

meta constant environment.is_recursive  :

Return tt iff the given name is a recursive inductive datatype

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

Return the constructors of the inductive datatype with the given name

meta constant environment.recursor_of  :

Return the recursor of the given inductive datatype

Return the number of parameters of the inductive datatype

Return the number of indices of the inductive datatype

Return tt iff the inductive datatype recursor supports dependent elimination

meta constant environment.is_ginductive  :

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.

See the docstring for projection_info.

meta constant environment.fold {α : Type} :
environmentα → (declarationα → α) → α

Fold over declarations in the environment.

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  :

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

meta constant environment.symm_for  :

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

meta constant environment.trans_for  :

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

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  :

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

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

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  :

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

Gets the equation lemmas for the declaration n.

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

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.

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

@[instance]