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 (__do_lift.sortFVarsByContextOrder 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

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

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

Check whether a metavariable is declared in the given MetavarContext.

Equations

• mctx.isExprMVarDeclared mvarId = mctx.decls.contains mvarId

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.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.isDeclared {m : Type → Type} [Monad m] [Lean.MonadMCtx m] (mvarId : Lean.MVarId) : m Bool

Check whether a metavariable is declared.

Equations

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

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

• mvarId.eraseAssignment = Lean.modifyMCtx fun (x : Lean.MetavarContext) => x.eraseExprMVarAssignment mvarId

def Lean.MVarId.synthInstance (g : Lean.MVarId) : Lean.MetaM Unit

Solve a goal by synthesizing an instance.

Equations

• g.synthInstance = do let __do_lift ← g.getType let __do_lift ← Lean.Meta.synthInstance __do_lift g.assign __do_lift

def Lean.MVarId.getTypeCleanup (mvarId : Lean.MVarId) : Lean.MetaM Lean.Expr

Get the type the given metavariable after instantiating metavariables and cleaning up annotations.

Equations

• mvarId.getTypeCleanup = do let __do_lift ← mvarId.getType let __do_lift ← Lean.instantiateMVars __do_lift pure __do_lift.cleanupAnnotations

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 (__do_lift.unassignedExprMVars 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.Options) => 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 <prefix>.<N> where N is a natural number. They are not suitable as user-facing names.

Equations

• Lean.Meta.mkFreshIdWithPrefix «prefix» = do let ngen ← Lean.getNGen let r : Lean.Name := { namePrefix := «prefix», idx := ngen.idx }.curr Lean.setNGen ngen.next pure r

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.