Structure methods that require MetaM
infrastructure #
If struct
is an application of the form S ..
with S
a constant for a structure,
returns the name of the structure, otherwise throws an error.
Equations
Instances For
Structure projection declaration for mkProjections
.
- ref : Syntax
- projName : Name
- paramInfoOverrides : List (Option BinderInfo)
Overrides to param binders to apply after param binder info inference.
Instances For
Adds projection functions to the environment for the one-constructor inductive type named n
.
- The
projName
s in eachStructProjDecl
are used for the names of the declarations added to the environment. - If
instImplicit
is true, then generates projections withself
being instance implicit.
Notes:
- This function supports everything that
Expr.proj
supports (seelean::type_checker::infer_proj
). This means we can generate projections for inductive types with one-constructor, even if it is an indexed family (which is not supported by thestructure
command). - We throw errors in the cases that
Expr.proj
is not type-correct.
Equations
Instances For
Given an expression e
that's either a native projection or a registered projection
function, gives the object being projected.
Checks that the parameters are defeq to params
, that the projection index is equal to idx
,
and, if x?
is provided, that the object being projected is equal to it.
Equations
Instances For
Eta reduces all structures satisfying p
in the whole expression.
See etaStruct?
for reducing single expressions.
Equations
Instances For
Instantiates the default value given by the default value function defaultFn
.
defaultFn
is the default value function returned byLean.getEffectiveDefaultFnForField?
orLean.getDefaultFnForField?
.levels?
is the list of levels to use, and otherwise the levels are inferred.params
is the list of structure parameters. These are assumed to be correct for the given levels.fieldVal?
is a function for getting fields for values, if they exist.
If successful, returns a set of fields used and the resulting default value. Success is expected. Callers should do metacontext backtracking themselves if needed.