def Lean.LocalDecl.setKind : Lean.LocalDecl → Lean.LocalDeclKind → Lean.LocalDecl

Set the kind of a LocalDecl.

Equations

• One or more equations did not get rendered due to their size.

def Lean.LocalContext.setKind (lctx : Lean.LocalContext) (fvarId : Lean.FVarId) (kind : Lean.LocalDeclKind) : Lean.LocalContext

Set the kind of the given fvar.

Equations

• Lean.LocalContext.setKind lctx fvarId kind = Lean.LocalContext.modifyLocalDecl lctx fvarId fun x => Lean.LocalDecl.setKind x kind

def Lean.LocalContext.sortFVarsByContextOrder (lctx : Lean.LocalContext) (hyps : Array Lean.FVarId) : Array Lean.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.

def Lean.Meta.sortFVarsByContextOrder {m : Type → Type} [Monad m] [Lean.MonadLCtx m] (hyps : Array Lean.FVarId) : m (Array Lean.FVarId)

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

Equations

• Lean.Meta.sortFVarsByContextOrder hyps = do let __do_lift ← Lean.getLCtx pure (Lean.LocalContext.sortFVarsByContextOrder __do_lift hyps)

def Lean.MetavarContext.getExprMVarDecl {m : Type → Type} [Monad m] [Lean.MonadError m] (mctx : Lean.MetavarContext) (mvarId : Lean.MVarId) : m Lean.MetavarDecl

Get the MetavarDecl of mvarId. If mvarId is not a declared metavariable in the given MetavarContext, throw an error.

Equations

• One or more equations did not get rendered due to their size.

def Lean.MetavarContext.declareExprMVar (mctx : Lean.MetavarContext) (mvarId : Lean.MVarId) (mdecl : Lean.MetavarDecl) : Lean.MetavarContext

Declare a metavariable. You must make sure that the metavariable is not already declared.

Equations

• One or more equations did not get rendered due to their size.

def Lean.MetavarContext.isExprMVarAssignedOrDelayedAssigned (mctx : Lean.MetavarContext) (mvarId : Lean.MVarId) : Bool

Check whether a metavariable is assigned or delayed-assigned. A delayed-assigned metavariable is already 'solved' but the solution cannot be substituted yet because we have to wait for some other metavariables to be assigned first. So in most situations you want to treat a delayed-assigned metavariable as assigned.

Equations

• Lean.MetavarContext.isExprMVarAssignedOrDelayedAssigned mctx mvarId = (Lean.PersistentHashMap.contains mctx.eAssignment mvarId || Lean.PersistentHashMap.contains mctx.dAssignment mvarId)

def Lean.MetavarContext.isExprMVarDeclared (mctx : Lean.MetavarContext) (mvarId : Lean.MVarId) : Bool

Check whether a metavariable is declared in the given MetavarContext.

Equations

• Lean.MetavarContext.isExprMVarDeclared mctx mvarId = Lean.PersistentHashMap.contains mctx.decls mvarId

def Lean.MetavarContext.delayedAssignExprMVar (mctx : Lean.MetavarContext) (mvarId : Lean.MVarId) (ass : Lean.DelayedMetavarAssignment) : Lean.MetavarContext

Add a delayed assignment for the given metavariable. You must make sure that the metavariable is not already assigned or delayed-assigned.

Equations

• One or more equations did not get rendered due to their size.

def Lean.MetavarContext.eraseExprMVarAssignment (mctx : Lean.MetavarContext) (mvarId : Lean.MVarId) : Lean.MetavarContext

Erase any assignment or delayed assignment of the given metavariable.

Equations

• One or more equations did not get rendered due to their size.

def Lean.MetavarContext.modifyExprMVarDecl (mctx : Lean.MetavarContext) (mvarId : Lean.MVarId) (f : Lean.MetavarDecl → Lean.MetavarDecl) : Lean.MetavarContext

Modify the declaration of a metavariable. If the metavariable is not declared, the MetavarContext is returned unchanged.

You must ensure that the modification is legal. In particular, expressions may only be replaced with defeq expressions.

Equations

• One or more equations did not get rendered due to their size.

def Lean.MetavarContext.modifyExprMVarLCtx (mctx : Lean.MetavarContext) (mvarId : Lean.MVarId) (f : Lean.LocalContext → Lean.LocalContext) : Lean.MetavarContext

Modify the local context of a metavariable. If the metavariable is not declared, the MetavarContext is returned unchanged.

You must ensure that the modification is legal. In particular, expressions may only be replaced with defeq expressions.

Equations

• One or more equations did not get rendered due to their size.

def Lean.MetavarContext.setFVarKind (mctx : Lean.MetavarContext) (mvarId : Lean.MVarId) (fvarId : Lean.FVarId) (kind : Lean.LocalDeclKind) : Lean.MetavarContext

Set the kind of an fvar. If the given metavariable is not declared or the given fvar doesn't exist in its context, the MetavarContext is returned unchanged.

Equations

• Lean.MetavarContext.setFVarKind mctx mvarId fvarId kind = Lean.MetavarContext.modifyExprMVarLCtx mctx mvarId fun x => Lean.LocalContext.setKind x fvarId kind

def Lean.MetavarContext.setFVarBinderInfo (mctx : Lean.MetavarContext) (mvarId : Lean.MVarId) (fvarId : Lean.FVarId) (bi : Lean.BinderInfo) : Lean.MetavarContext

Set the BinderInfo of an fvar. If the given metavariable is not declared or the given fvar doesn't exist in its context, the MetavarContext is returned unchanged.

Equations

• Lean.MetavarContext.setFVarBinderInfo mctx mvarId fvarId bi = Lean.MetavarContext.modifyExprMVarLCtx mctx mvarId fun x => Lean.LocalContext.setBinderInfo x fvarId bi

def Lean.MetavarContext.unassignedExprMVars (mctx : Lean.MetavarContext) (includeDelayed : optParam Bool false) : Array Lean.MVarId

Obtain all unassigned metavariables from the given MetavarContext. If includeDelayed is true, delayed-assigned metavariables are considered unassigned.

Equations

• One or more equations did not get rendered due to their size.

def Lean.MVarId.isAssignedOrDelayedAssigned {m : Type → Type} [Monad m] [Lean.MonadMCtx m] (mvarId : Lean.MVarId) : m Bool

Check whether a metavariable is assigned or delayed-assigned. A delayed-assigned metavariable is already 'solved' but the solution cannot be substituted yet because we have to wait for some other metavariables to be assigned first. So in most situations you want to treat a delayed-assigned metavariable as assigned.

Equations

• Lean.MVarId.isAssignedOrDelayedAssigned mvarId = do let __do_lift ← Lean.getMCtx pure (Lean.MetavarContext.isExprMVarAssignedOrDelayedAssigned __do_lift mvarId)

def Lean.MVarId.isDeclared {m : Type → Type} [Monad m] [Lean.MonadMCtx m] (mvarId : Lean.MVarId) : m Bool

Check whether a metavariable is declared.

Equations

• Lean.MVarId.isDeclared mvarId = do let __do_lift ← Lean.getMCtx pure (Lean.MetavarContext.isExprMVarDeclared __do_lift mvarId)

def Lean.MVarId.delayedAssign {m : Type → Type} [Lean.MonadMCtx m] (mvarId : Lean.MVarId) (ass : Lean.DelayedMetavarAssignment) : m Unit

Add a delayed assignment for the given metavariable. You must make sure that the metavariable is not already assigned or delayed-assigned.

Equations

• Lean.MVarId.delayedAssign mvarId ass = Lean.modifyMCtx fun x => Lean.MetavarContext.delayedAssignExprMVar x mvarId ass

def Lean.MVarId.eraseAssignment {m : Type → Type} [Lean.MonadMCtx m] (mvarId : Lean.MVarId) : m Unit

Erase any assignment or delayed assignment of the given metavariable.

Equations

• Lean.MVarId.eraseAssignment mvarId = Lean.modifyMCtx fun x => Lean.MetavarContext.eraseExprMVarAssignment x mvarId

def Lean.MVarId.modifyDecl {m : Type → Type} [Lean.MonadMCtx m] (mvarId : Lean.MVarId) (f : Lean.MetavarDecl → Lean.MetavarDecl) : m Unit

Modify the declaration of a metavariable. If the metavariable is not declared, nothing happens.

You must ensure that the modification is legal. In particular, expressions may only be replaced with defeq expressions.

Equations

• Lean.MVarId.modifyDecl mvarId f = Lean.modifyMCtx fun x => Lean.MetavarContext.modifyExprMVarDecl x mvarId f

def Lean.MVarId.modifyLCtx {m : Type → Type} [Lean.MonadMCtx m] (mvarId : Lean.MVarId) (f : Lean.LocalContext → Lean.LocalContext) : m Unit

Modify the local context of a metavariable. If the metavariable is not declared, nothing happens.

You must ensure that the modification is legal. In particular, expressions may only be replaced with defeq expressions.

Equations

• Lean.MVarId.modifyLCtx mvarId f = Lean.modifyMCtx fun x => Lean.MetavarContext.modifyExprMVarLCtx x mvarId f

def Lean.MVarId.setFVarKind {m : Type → Type} [Lean.MonadMCtx m] (mvarId : Lean.MVarId) (fvarId : Lean.FVarId) (kind : Lean.LocalDeclKind) : m Unit

Set the kind of an fvar. If the given metavariable is not declared or the given fvar doesn't exist in its context, nothing happens.

Equations

• Lean.MVarId.setFVarKind mvarId fvarId kind = Lean.modifyMCtx fun x => Lean.MetavarContext.setFVarKind x mvarId fvarId kind

def Lean.MVarId.setFVarBinderInfo {m : Type → Type} [Lean.MonadMCtx m] (mvarId : Lean.MVarId) (fvarId : Lean.FVarId) (bi : Lean.BinderInfo) : m Unit

Set the BinderInfo of an fvar. If the given metavariable is not declared or the given fvar doesn't exist in its context, nothing happens.

Equations

• Lean.MVarId.setFVarBinderInfo mvarId fvarId bi = Lean.modifyMCtx fun x => Lean.MetavarContext.setFVarBinderInfo x mvarId fvarId bi

def Lean.MVarId.getMVarDependencies (mvarId : Lean.MVarId) (includeDelayed : optParam Bool false) : Lean.MetaM (Lean.HashSet Lean.MVarId)

Collect the metavariables which mvarId depends on. These are the metavariables which appear in the type and local context of mvarId, as well as the metavariables which those metavariables depend on, etc.

Equations

• Lean.MVarId.getMVarDependencies mvarId includeDelayed = (fun x => x.snd) <$> StateRefT'.run (Lean.MVarId.getMVarDependencies.go includeDelayed mvarId) ∅

partial def Lean.MVarId.getMVarDependencies.addMVars (includeDelayed : optParam Bool false) (e : Lean.Expr) : StateRefT' IO.RealWorld (Lean.HashSet Lean.MVarId) Lean.MetaM Unit

Auxiliary definition for getMVarDependencies.

partial def Lean.MVarId.getMVarDependencies.go (includeDelayed : optParam Bool false) (mvarId : Lean.MVarId) : StateRefT' IO.RealWorld (Lean.HashSet Lean.MVarId) Lean.MetaM Unit

Auxiliary definition for getMVarDependencies.

def Lean.Meta.getUnassignedExprMVars {m : Type → Type} [Monad m] [Lean.MonadMCtx m] (includeDelayed : optParam Bool false) : m (Array Lean.MVarId)

Obtain all unassigned metavariables. If includeDelayed is true, delayed-assigned metavariables are considered unassigned.

Equations

• Lean.Meta.getUnassignedExprMVars includeDelayed = do let __do_lift ← Lean.getMCtx pure (Lean.MetavarContext.unassignedExprMVars __do_lift includeDelayed)

def Lean.Meta.unhygienic {m : Type → Type} {α : Type} [Lean.MonadWithOptions m] (x : m α) : m α

Run a computation with hygiene turned off.

Equations

• Lean.Meta.unhygienic x = Lean.withOptions (fun x => Lean.Option.set x Lean.Meta.tactic.hygienic false) x

def Lean.Meta.mkFreshIdWithPrefix {m : Type → Type} [Monad m] [Lean.MonadNameGenerator m] (prefix : Lean.Name) : m Lean.Name

A variant of mkFreshId which generates names with a particular prefix. The generated names are unique and have the form . where N is a natural number. They are not suitable as user-facing names.

Equations

• One or more equations did not get rendered due to their size.

def Lean.Meta.repeat'Core {m : Type → Type} [Monad m] [Lean.MonadError m] [Lean.MonadMCtx m] (f : Lean.MVarId → m (List Lean.MVarId)) (gs : List Lean.MVarId) (maxIters : optParam Nat 100000) : m (Bool × List Lean.MVarId)

Implementation of repeat' and repeat1'.

repeat'Core f runs f on all of the goals to produce a new list of goals, then runs f again on all of those goals, and repeats until f fails on all remaining goals, or until maxIters total calls to f have occurred.

Returns a boolean indicating whether f succeeded at least once, and all the remaining goals (i.e. those on which f failed).

Equations

• One or more equations did not get rendered due to their size.

def Lean.Meta.repeat'Core.go {m : Type → Type} [Monad m] [Lean.MonadError m] [Lean.MonadMCtx m] (f : Lean.MVarId → m (List Lean.MVarId)) : Nat → Bool → List Lean.MVarId → List (List Lean.MVarId) → Array Lean.MVarId → m (Bool × Array Lean.MVarId)

Auxiliary for repeat'Core. repeat'Core.go f maxIters progress gs stk acc evaluates to essentially acc.toList ++ repeat' f (gs::stk).join maxIters: that is, acc are goals we will not revisit, and (gs::stk).join is the accumulated todo list of subgoals.

Equations

• One or more equations did not get rendered due to their size.
• Lean.Meta.repeat'Core.go f x x [] [] x = pure (x, x)
• Lean.Meta.repeat'Core.go f x x [] (gs :: stk) x = Lean.Meta.repeat'Core.go f x x gs stk x

def Lean.Meta.repeat' {m : Type → Type} [Monad m] [Lean.MonadError m] [Lean.MonadMCtx m] (f : Lean.MVarId → m (List Lean.MVarId)) (gs : List Lean.MVarId) (maxIters : optParam Nat 100000) : m (List Lean.MVarId)

repeat' f runs f on all of the goals to produce a new list of goals, then runs f again on all of those goals, and repeats until f fails on all remaining goals, or until maxIters total calls to f have occurred. Always succeeds (returning the original goals if f fails on all of them).

Equations

• Lean.Meta.repeat' f gs maxIters = Lean.Meta.repeat'Core f gs maxIters <&> fun x => x.snd

def Lean.Meta.repeat1' {m : Type → Type} [Monad m] [Lean.MonadError m] [Lean.MonadMCtx m] (f : Lean.MVarId → m (List Lean.MVarId)) (gs : List Lean.MVarId) (maxIters : optParam Nat 100000) : m (List Lean.MVarId)

repeat1' f runs f on all of the goals to produce a new list of goals, then runs f again on all of those goals, and repeats until f fails on all remaining goals, or until maxIters total calls to f have occurred. Fails if f does not succeed at least once.

Equations

• One or more equations did not get rendered due to their size.

def Lean.Meta.saturate1 {m : Type → Type} [Monad m] [Lean.MonadError m] [Lean.MonadRecDepth m] [MonadLiftT (ST IO.RealWorld) m] (goal : Lean.MVarId) (tac : Lean.MVarId → m (Option (Array Lean.MVarId))) : m (Option (Array Lean.MVarId))

saturate1 goal tac runs tac on goal, then on the resulting goals, etc., until tac does not apply to any goal any more (i.e. it returns none). The order of applications is depth-first, so if tac generates goals [g₁, g₂, ⋯], we apply tac to g₁ and recursively to all its subgoals before visiting g₂. If tac does not apply to goal, saturate1 returns none. Otherwise it returns the generated subgoals to which tac did not apply. saturate1 respects the MonadRecDepth recursion limit.

Equations

• One or more equations did not get rendered due to their size.

partial def Lean.Meta.saturate1.go {m : Type → Type} [Monad m] [Lean.MonadError m] [Lean.MonadRecDepth m] [MonadLiftT (ST IO.RealWorld) m] (tac : Lean.MVarId → m (Option (Array Lean.MVarId))) (acc : IO.Ref (Array Lean.MVarId)) (goal : Lean.MVarId) : m Unit

Auxiliary definition for saturate1.