mathlib documentation

core / init.meta.local_context

source
meta structure local_decl  :
Type
source
meta def local_decl.to_expr  :
local_decl → expr
source
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.

source
meta constant local_context.empty  :
local_context

The empty local context.

source
meta constant local_context.mk_local (pretty_name : name) (type : expr) (bi : 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.

source
meta constant local_context.get_local_decl  :
name → local_context → option local_decl
source
meta constant local_context.get_local  :
name → local_context → option expr
source
meta constant local_context.is_subset  :
local_context → local_context → bool
source
@[instance]
meta constant local_context.has_decidable_eq  :
decidable_eq local_context
source
meta constant local_context.fold {α : Type} (f : α → expr → α) :
α → local_context → α
source
meta def local_context.to_list  :
local_context → list expr
source
meta def local_context.to_format  :
local_context → format
source
@[protected, instance]
meta def local_context.has_to_format  :
has_to_format local_context
source
@[protected, instance]
meta def local_context.has_le  :
has_le local_context
source
@[protected, instance]
meta def local_context.decidable_rel  :
decidable_rel has_le.le
source
@[protected, instance]
meta def local_context.has_emptyc  :
has_emptyc local_context
source
@[protected, instance]
meta def local_context.inhabited  :
inhabited local_context
source
@[protected, instance]
meta def local_context.has_mem  :
has_mem expr local_context
source
@[protected, instance]
meta def local_context.has_mem.mem.decidable {e : expr} {lc : local_context} :
decidable (e ∈ lc)