An __environment__ contains all of the declarations and notation that have been defined so far.
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:
cnameis the name of the constructor associated with the projection.nparamsis the number of constructor parameters. Egand.introhas two type parameters.idxis the parameter being projected by this projection.is_classis tt iff this is a typeclass projection.
Examples:
and.rightis a projection with{cname := `and.intro, nparams := 2, idx := 1, is_class := ff}ordered_ring.negis a projection with{cname := `ordered_ring.mk, nparams := 1, idx := 5, is_class := tt}.
- 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)
- constr : name
- type : expr
- infer : environment.implicit_infer_kind
One introduction rule in an inductive declaration
Create a standard environment using the given trust level
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
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
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).
Return tt iff the given name is an inductive datatype
Return tt iff the given name is a constructor
Return tt iff the given name is a recursor
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
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
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.
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.
refl_for env R returns the name of the reflexivity theorem for the relation R
symm_for env R returns the name of the symmetry theorem for the relation R
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.
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]
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