A local context is a list of local constant declarations. Each metavariable in a metavariable context holds a local_context to declare which locals the metavariable is allowed to depend on.
constant
local_context.mk_local
:
name → expr → binder_info → local_context → option (expr × local_context)
Add a new local constant to the lc. The new local has an unused unique_name. Fails when the type depends on local constants that are not present in the context.
@[instance]