mathlib documentation

core.init.meta.local_context

meta structure local_decl :

Type

unique_name : name
pp_name : name
type : expr
value : option expr
bi : binder_info
idx : ℕ

meta def local_decl.to_expr (a : local_decl) :

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.

meta constant local_context.empty :

The empty local context.

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

meta constant local_context.get_local_decl (a : name) (a_1 : local_context) :

option local_decl

meta constant local_context.get_local (a : name) (a_1 : local_context) :

meta constant local_context.is_subset (a a_1 : local_context) :

@[instance]

meta constant local_context.has_decidable_eq :

decidable_eq local_context

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

α

meta def local_context.to_list (a : local_context) :

meta def local_context.to_format (a : local_context) :

@[instance]

meta def local_context.has_to_format :

has_to_format local_context

@[instance]

meta def local_context.has_le :

has_le local_context

@[instance]

meta def local_context.decidable_rel :

decidable_rel has_le.le

@[instance]

meta def local_context.has_emptyc :

has_emptyc local_context

@[instance]

meta def local_context.inhabited :

inhabited local_context

@[instance]

meta def local_context.has_mem :

has_mem expr local_context

@[instance]

meta def local_context.decidable {e : expr} {lc : local_context} :

decidable (e ∈ lc)