Documentation

Lean.LocalContext

source
inductive Lean.LocalDeclKind :
Type

Whether a local declaration should be found by type class search, tactics, etc. and shown in the goal display.

  • default : LocalDeclKind

    Participates fully in type class search, tactics, and is shown even if inaccessible.

    For example: the x in fun x => _ has the default kind.

  • implDetail : LocalDeclKind

    Invisible to type class search or tactics, and hidden in the goal display.

    This kind is used for temporary variables in macros. For example: return (← foo) + bar expands to foo >>= fun __tmp => pure (__tmp + bar), where __tmp has the implDetail kind.

  • auxDecl : LocalDeclKind

    Auxiliary local declaration for recursive calls. The behavior is similar to implDetail.

    For example: def foo (n : Nat) : Nat := _ adds the local declaration foo : Nat → Nat to allow recursive calls. This declaration has the auxDecl kind.

Instances For
source
instance Lean.instInhabitedLocalDeclKind :
Inhabited LocalDeclKind
Equations
source
instance Lean.instReprLocalDeclKind :
Repr LocalDeclKind
Equations
source
instance Lean.instDecidableEqLocalDeclKind :
DecidableEq LocalDeclKind
Equations
source
instance Lean.instHashableLocalDeclKind :
Hashable LocalDeclKind
Equations
source
inductive Lean.LocalDecl :
Type

A declaration for a LocalContext. This is used to register which free variables are in scope.

See LocalDecl.index, LocalDecl.fvarId, LocalDecl.userName, LocalDecl.type for accessors for arguments common to both constructors.

  • cdecl (index : Nat) (fvarId : FVarId) (userName : Name) (type : Expr) (bi : BinderInfo) (kind : LocalDeclKind) : LocalDecl

    A local variable without any value. Lean.LocalContext.mkBinding creates lambdas or foralls from cdecls.

  • ldecl (index : Nat) (fvarId : FVarId) (userName : Name) (type value : Expr) (nondep : Bool) (kind : LocalDeclKind) : LocalDecl

    A let-bound free variable, with a value value : Expr. If nondep := false, then the variable is definitionally equal to its value. If nondep := true, then the variable has an opaque value; we call these "have-bound free variables." Lean.LocalContext.mkBinding creates let/have expressions from ldecls.

    Important: The nondep := true case is subtle; it is not merely an opaque ldecl!

    • In most contexts, nondependent ldecls should be treated like cdecls. For example, suppose we have a tactic goal x : α := v (nondep) ⊢ b. It would be incorrect for revert x to produce the goal ⊢ have x : α := v; b, since this would be saying "to prove b without knowledge of the value of x, it suffices to prove have x : α := v; b for this particular value of x." Instead, revert x must produce the goal ⊢ ∀ x : α, b. Furthermore, given a goal ⊢ have x : α := v; b, the intro x tactic should yield a dependent ldecl, since users expect to be able to make use of the value of x, plus, as discussed, if intro yielded a nondep ldecl then intro x; revert x would convert the goal into a forall, not a have.
    • Also: value might not be type correct. Metaprograms may decide to pretend that all nondep := true ldecls are cdecls (for example, when reverting variables). As a consequence, nondep ldecls may have type-incorrect values. This design decision allows metaprograms to not have to think about nondep ldecls, so long as LocalDecl values are consumed through LocalDecl.isLet and LocalDecl.value? with (allowNondep := false). Rule: never use (generalizeNondepLet := false) in mkBinding-family functions within a local context you do not own. See LocalDecl.setNondep for some additional discussion.
    • Where then do nondep ldecls come from? Common functions are Meta.mapLetDecl, Meta.withLetDecl, and Meta.letTelescope. The have term syntax makes use of a nondep ldecl as well.

    Therefore, nondep := true should be used with consideration. Its primary use is in metaprograms that enter let/have telescopes and wish to reconstruct them.

Instances For
source
instance Lean.instInhabitedLocalDecl :
Inhabited LocalDecl
Equations
source
@[export lean_mk_local_decl]
def Lean.mkLocalDeclEx (index : Nat) (fvarId : FVarId) (userName : Name) (type : Expr) (bi : BinderInfo) :
LocalDecl
Equations
source
@[export lean_mk_let_decl]
def Lean.mkLetDeclEx (index : Nat) (fvarId : FVarId) (userName : Name) (type val : Expr) :
LocalDecl
Equations
source
@[export lean_local_decl_binder_info]
def Lean.LocalDecl.binderInfoEx :
LocalDecl → BinderInfo
Equations
source
def Lean.LocalDecl.isLet :
LocalDecl → (allowNondep : optParam Bool false) → Bool

Returns true if this is an ldecl with a visible value.

If allowNondep is true then includes ldecls with nondep := true, whose values are normally hidden.

Equations
source
def Lean.LocalDecl.index :
LocalDecl → Nat

The position of the decl in the local context.

Equations
source
def Lean.LocalDecl.setIndex :
LocalDecl → Nat → LocalDecl
Equations
source
def Lean.LocalDecl.fvarId :
LocalDecl → FVarId

The unique id of the free variable.

Equations
source
def Lean.LocalDecl.userName :
LocalDecl → Name

The pretty-printable name of the variable.

Equations
source
def Lean.LocalDecl.type :
LocalDecl → Expr

The type of the variable.

Equations
source
def Lean.LocalDecl.setType :
LocalDecl → Expr → LocalDecl
Equations
source
def Lean.LocalDecl.binderInfo :
LocalDecl → BinderInfo
Equations
source
def Lean.LocalDecl.kind :
LocalDecl → LocalDeclKind
Equations
source
def Lean.LocalDecl.isAuxDecl (d : LocalDecl) :
Bool
Equations
source
def Lean.LocalDecl.isImplementationDetail (d : LocalDecl) :
Bool

Is the local declaration an implementation-detail hypothesis (including auxiliary declarations)?

Equations
source
def Lean.LocalDecl.value? :
LocalDecl → (allowNondep : optParam Bool false) → Option Expr

Returns the value of the ldecl if it has a visible value.

If allowNondep is true, then allows nondependent ldecls, whose values are normally hidden.

Equations
source
def Lean.LocalDecl.value :
LocalDecl → (allowNondep : optParam Bool false) → Expr

Returns the value of the ldecl if it has a visible value.

If allowNondep is true, then allows nondependent ldecls, whose values are normally hidden.

Equations
source
def Lean.LocalDecl.hasValue :
LocalDecl → (allowNondep : optParam Bool false) → Bool

Returns true if LocalDecl.value? is not none.

Equations
source
def Lean.LocalDecl.setValue :
LocalDecl → Expr → LocalDecl

Sets the value of an ldecl, otherwise returns cdecls unchanged.

Equations
source
def Lean.LocalDecl.setNondep :
LocalDecl → Bool → LocalDecl

Sets the nondep flag of an ldecl, otherwise returns cdecls unchanged.

This is a low-level function, and it is the responsibility of the caller to ensure that transitions of nondep are valid.

Rules:

  • If the declaration is not under the caller's control, then setting nondep := false must not be done. General nondependent ldecls should be treated like cdecls. See also the docstring for LocalDecl.ldecl about the value not necessarily being type correct.
  • Setting nondep := true is usually fine.
    • Caution: be sure any relevant caches are cleared so that the value associated to this FVarId does not leak.
    • Caution: be sure that metavariables dependent on this declaration created before and after the transition are not mixed, since unification does not check "nondep-compatibility" of local contexts when assigning metavariables.

For example, setting nondep := false is fine from within a telescope combinator, to update the local context right before calling mkLetFVars:

let lctx ← getLCtx
letTelescope e fun xs b => do
  let lctx' ← xs.foldlM (init := lctx) fun lctx' x => do
    let decl ← x.fvarId!.getDecl
    -- Clear the flag if it's not a prop.
    let decl' := decl.setNondep <| ← pure decl.isNondep <&&> Meta.isProp decl.type
    pure <| lctx'.addDecl decl'
  withLCtx' lctx' do
    mkLetFVars (usedLetOnly := false) (generalizeNondepLet := false) xs b
  1. The declarations for xs are in the control of this metaprogram.
  2. mkLetFVars does make use of MetaM caches.
  3. Even if e has metavariables, these do not include xs in their contexts, so the change of the nondep flag does not cause any issues in the abstractM system used by mkLetFVars.
Equations
source
def Lean.LocalDecl.isNondep :
LocalDecl → Bool

Returns true if this is an ldecl with nondep := true.

Equations
source
def Lean.LocalDecl.setUserName :
LocalDecl → Name → LocalDecl
Equations
source
def Lean.LocalDecl.setBinderInfo :
LocalDecl → BinderInfo → LocalDecl
Equations
source
def Lean.LocalDecl.toExpr (decl : LocalDecl) :
Expr
Equations
source
def Lean.LocalDecl.hasExprMVar :
LocalDecl → Bool
Equations
source
def Lean.LocalDecl.setKind :
LocalDecl → LocalDeclKind → LocalDecl

Set the kind of a LocalDecl.

Equations
source
structure Lean.LocalContext :
Type

A LocalContext is an ordered set of local variable declarations. It is used to store the free variables (also known as local constants) that are in scope. It also maps free variables corresponding to auxiliary declarations (recursive references and where and let rec bindings) to their fully-qualified global names.

When inspecting a goal or expected type in the infoview, the local context is all of the variables above the ⊢ symbol.

Instances For
source
instance Lean.instInhabitedLocalContext :
Inhabited LocalContext
Equations
source
@[export lean_mk_empty_local_ctx]
def Lean.LocalContext.mkEmpty :
Unit → LocalContext
Equations
source
def Lean.LocalContext.empty :
LocalContext
Equations
source
@[export lean_local_ctx_is_empty]
def Lean.LocalContext.isEmpty (lctx : LocalContext) :
Bool
Equations
source
def Lean.LocalContext.mkLocalDecl (lctx : LocalContext) (fvarId : FVarId) (userName : Name) (type : Expr) (bi : BinderInfo := BinderInfo.default) (kind : LocalDeclKind := LocalDeclKind.default) :
LocalContext

Low level API for creating local declarations (LocalDecl.cdecl). It is used to implement actions in the monads Elab and Tactic. It should not be used directly since the argument (fvarId : FVarId) is assumed to be unique. You can create a unique fvarId with mkFreshFVarId.

Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.LocalContext.mkLetDecl (lctx : LocalContext) (fvarId : FVarId) (userName : Name) (type value : Expr) (nondep : Bool := false) (kind : LocalDeclKind := default) :
LocalContext

Low level API for let declarations. Do not use directly.

Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.LocalContext.mkAuxDecl (lctx : LocalContext) (fvarId : FVarId) (userName : Name) (type : Expr) (fullName : Name) :
LocalContext

Low level API for auxiliary declarations. Do not use directly.

Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.LocalContext.addDecl (lctx : LocalContext) (newDecl : LocalDecl) :
LocalContext

Low level API for adding a local declaration. Do not use directly.

Equations
  • One or more equations did not get rendered due to their size.
source
@[export lean_local_ctx_find]
def Lean.LocalContext.find? (lctx : LocalContext) (fvarId : FVarId) :
Option LocalDecl
Equations
source
def Lean.LocalContext.findFVar? (lctx : LocalContext) (e : Expr) :
Option LocalDecl
Equations
source
def Lean.LocalContext.get! (lctx : LocalContext) (fvarId : FVarId) :
LocalDecl
Equations
source
def Lean.LocalContext.getFVar! (lctx : LocalContext) (e : Expr) :
LocalDecl

Gets the declaration for expression e in the local context. If e is not a free variable or not present then panics.

Equations
source
def Lean.LocalContext.contains (lctx : LocalContext) (fvarId : FVarId) :
Bool
Equations
source
def Lean.LocalContext.containsFVar (lctx : LocalContext) (e : Expr) :
Bool

Returns true when the lctx contains the free variable e. Panics if e is not an fvar.

Equations
source
def Lean.LocalContext.getFVarIds (lctx : LocalContext) :
Array FVarId
Equations
source
def Lean.LocalContext.getFVars (lctx : LocalContext) :
Array Expr

Return all of the free variables in the given context.

Equations
source
@[export lean_local_ctx_erase]
def Lean.LocalContext.erase (lctx : LocalContext) (fvarId : FVarId) :
LocalContext
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.LocalContext.pop (lctx : LocalContext) :
LocalContext
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.LocalContext.findFromUserName? (lctx : LocalContext) (userName : Name) :
Option LocalDecl
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.LocalContext.usesUserName (lctx : LocalContext) (userName : Name) :
Bool
Equations
source
def Lean.LocalContext.getUnusedName (lctx : LocalContext) (suggestion : Name) :
Name
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.LocalContext.lastDecl (lctx : LocalContext) :
Option LocalDecl
Equations
source
def Lean.LocalContext.setUserName (lctx : LocalContext) (fvarId : FVarId) (userName : Name) :
LocalContext
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.LocalContext.renameUserName (lctx : LocalContext) (fromName toName : Name) :
LocalContext
Equations
  • One or more equations did not get rendered due to their size.
source
@[inline]
def Lean.LocalContext.modifyLocalDecl (lctx : LocalContext) (fvarId : FVarId) (f : LocalDecl → LocalDecl) :
LocalContext

Low-level function for updating the local context. Assumptions about f, the resulting nested expressions must be definitionally equal to their original values, the index nor fvarId are modified.

Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.LocalContext.setKind (lctx : LocalContext) (fvarId : FVarId) (kind : LocalDeclKind) :
LocalContext

Set the kind of the given fvar.

Equations
source
def Lean.LocalContext.setBinderInfo (lctx : LocalContext) (fvarId : FVarId) (bi : BinderInfo) :
LocalContext
Equations
source
@[export lean_local_ctx_num_indices]
def Lean.LocalContext.numIndices (lctx : LocalContext) :
Nat
Equations
source
def Lean.LocalContext.getAt? (lctx : LocalContext) (i : Nat) :
Option LocalDecl
Equations
source
@[specialize #[]]
def Lean.LocalContext.foldlM {m : Type u_1 → Type u_2} {β : Type u_1} [Monad m] (lctx : LocalContext) (f : β → LocalDecl → m β) (init : β) (start : Nat := 0) :
m β
Equations
source
@[specialize #[]]
def Lean.LocalContext.foldrM {m : Type u_1 → Type u_2} {β : Type u_1} [Monad m] (lctx : LocalContext) (f : LocalDecl → β → m β) (init : β) :
m β
Equations
source
@[specialize #[]]
def Lean.LocalContext.forM {m : Type u_1 → Type u_2} [Monad m] (lctx : LocalContext) (f : LocalDecl → m PUnit) :
m PUnit
Equations
source
@[specialize #[]]
def Lean.LocalContext.findDeclM? {m : Type u_1 → Type u_2} {β : Type u_1} [Monad m] (lctx : LocalContext) (f : LocalDecl → m (Option β)) :
m (Option β)
Equations
source
@[specialize #[]]
def Lean.LocalContext.findDeclRevM? {m : Type u_1 → Type u_2} {β : Type u_1} [Monad m] (lctx : LocalContext) (f : LocalDecl → m (Option β)) :
m (Option β)
Equations
source
instance Lean.LocalContext.instForInLocalDecl {m : Type u_1 → Type u_2} :
ForIn m LocalContext LocalDecl
Equations
  • One or more equations did not get rendered due to their size.
source
@[inline]
def Lean.LocalContext.foldl {β : Type u_1} (lctx : LocalContext) (f : β → LocalDecl → β) (init : β) (start : Nat := 0) :
β
Equations
source
@[inline]
def Lean.LocalContext.foldr {β : Type u_1} (lctx : LocalContext) (f : LocalDecl → β → β) (init : β) :
β
Equations
source
def Lean.LocalContext.size (lctx : LocalContext) :
Nat
Equations
source
@[inline]
def Lean.LocalContext.findDecl? {β : Type u_1} (lctx : LocalContext) (f : LocalDecl → Option β) :
Option β
Equations
source
@[inline]
def Lean.LocalContext.findDeclRev? {β : Type u_1} (lctx : LocalContext) (f : LocalDecl → Option β) :
Option β
Equations
source
partial def Lean.LocalContext.isSubPrefixOfAux (a₁ a₂ : PArray (Option LocalDecl)) (exceptFVars : Array Expr) (i j : Nat) :
Bool
source
def Lean.LocalContext.isSubPrefixOf (lctx₁ lctx₂ : LocalContext) (exceptFVars : Array Expr := #[]) :
Bool

Given lctx₁ - exceptFVars of the form (x_1 : A_1) ... (x_n : A_n), then return true iff there is a local context B_1* (x_1 : A_1) ... B_n* (x_n : A_n) which is a prefix of lctx₂ where B_i's are (possibly empty) sequences of local declarations.

Equations
source
@[inline]
def Lean.LocalContext.mkBinding (isLambda : Bool) (lctx : LocalContext) (xs : Array Expr) (b : Expr) (generalizeNondepLet : Bool := false) :
Expr
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.LocalContext.mkLambda (lctx : LocalContext) (xs : Array Expr) (b : Expr) (generalizeNondepLet : Bool := false) :
Expr

Creates the expression fun x₁ .. xₙ => b for free variables xs = #[x₁, .., xₙ], suitably abstracting b and the types for each of the xᵢ.

Equations
source
def Lean.LocalContext.mkForall (lctx : LocalContext) (xs : Array Expr) (b : Expr) (generalizeNondepLet : Bool := false) :
Expr

Creates the expression (x₁:α₁) → .. → (xₙ:αₙ) → b for free variables xs = #[x₁, .., xₙ], suitably abstracting b and the types for each of the xᵢ, αᵢ.

Equations
source
@[inline]
def Lean.LocalContext.anyM {m : Type → Type u_1} [Monad m] (lctx : LocalContext) (p : LocalDecl → m Bool) :
m Bool
Equations
source
@[inline]
def Lean.LocalContext.allM {m : Type → Type u_1} [Monad m] (lctx : LocalContext) (p : LocalDecl → m Bool) :
m Bool
Equations
source
@[inline]
def Lean.LocalContext.any (lctx : LocalContext) (p : LocalDecl → Bool) :
Bool

Return true if lctx contains a local declaration satisfying p.

Equations
source
@[inline]
def Lean.LocalContext.all (lctx : LocalContext) (p : LocalDecl → Bool) :
Bool

Return true if all declarations in lctx satisfy p.

Equations
source
def Lean.LocalContext.sanitizeNames (lctx : LocalContext) :
StateM NameSanitizerState LocalContext

If option pp.sanitizeNames is set to true, add tombstone to shadowed local declaration names and ones contains macroscopes.

Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.LocalContext.getRoundtrippingUserName? (lctx : LocalContext) (fvarId : FVarId) :
Option Name

Given an FVarId, this function returns the corresponding user name, but only if the name can be used to recover the original FVarId.

Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.LocalContext.sortFVarsByContextOrder (lctx : LocalContext) (hyps : Array FVarId) :
Array FVarId

Sort the given FVarIds by the order in which they appear in lctx. If any of the FVarIds do not appear in lctx, the result is unspecified.

Equations
  • One or more equations did not get rendered due to their size.
source
class Lean.MonadLCtx (m : Type → Type) :
Type

Class used to denote that m has a local context.

Instances
source
instance Lean.instMonadLCtxOfMonadLift {m n : Type → Type} [MonadLift m n] [MonadLCtx m] :
MonadLCtx n
Equations
source
def Lean.getLocalHyps {m : Type → Type} [Monad m] [MonadLCtx m] :
m (Array Expr)

Return local hypotheses which are not "implementation detail", as Exprs.

Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.LocalDecl.replaceFVarId (fvarId : FVarId) (e : Expr) (d : LocalDecl) :
LocalDecl
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.LocalContext.replaceFVarId (fvarId : FVarId) (e : Expr) (lctx : LocalContext) :
LocalContext
Equations
  • One or more equations did not get rendered due to their size.