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.

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} :
(α → expr → α)α → local_context → α

@[instance]

@[instance]
meta def local_context.decidable {e : expr} {lc : local_context} :
decidable (e lc)