mathlib documentation

core / init.meta.local_context

meta structure local_decl  :
Type

meta constant local_context  :
Type

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.

The empty local context.

meta constant local_context.mk_local (pretty_name : name) (type : expr) (bi : binder_info) :

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.

meta constant local_context.fold {α : Type} (f : α → expr → α) :
α → local_context → α

@[instance]

@[instance]