The following functions let us run MetaM actions in the context of a rapp or goal. Rapps save the metavariable context in which they were run by storing a Meta.SavedState. When we, for example, apply a rule to a goal, we run the rule's action in the metavariable context of the goal (which is the metavariable context of the goal's parent rapp). The resulting metavariable context, in which the goal mvar is assigned to an expression generated by the rule, then becomes the metavariable context of the rule's rapp.

To save and restore metavariable contexts, we use the MonadBacktrack MetaM instance. This means that some elements of the state are persistent, notably caches and trace messages. These become part of the global state.

The environment is not persistent. This means that modifications of the environment made by a rule are not visible in the global state and are reset once the tactic exits. As a result, rules which modify the environment are likely to fail.

@[implicit_reducible]

def Aesop.instMonadLiftTSTRealWorld_aesop {m : Type → Type u_1} [MonadLiftT Lean.MetaM m] : MonadLiftT (ST IO.RealWorld) m

Equations

• Aesop.instMonadLiftTSTRealWorld_aesop = { monadLift := fun {α : Type} (x : ST IO.RealWorld α) => liftM (liftM x) }

def Aesop.Rapp.runMetaM' {m : Type → Type u_1} [Monad m] [MonadLiftT Lean.MetaM m] [MonadFinally m] {α : Type} (x : m α) (r : Rapp) : m α

Equations

• Aesop.Rapp.runMetaM' x r = Aesop.runInMetaState r.metaState x

def Aesop.Rapp.runMetaM {m : Type → Type u_1} [Monad m] [MonadLiftT Lean.MetaM m] [MonadFinally m] {α : Type} (x : m α) (r : Rapp) : m (α × Lean.Meta.SavedState)

Equations

• Aesop.Rapp.runMetaM x r = Aesop.Rapp.runMetaM' (Aesop.withSaveState✝ x) r

def Aesop.Rapp.runMetaMModifying {m : Type → Type u_1} [Monad m] [MonadLiftT Lean.MetaM m] [MonadFinally m] {α : Type} (x : m α) (r : Rapp) : m (α × Rapp)

Equations

• Aesop.Rapp.runMetaMModifying x r = do let __discr ← Aesop.Rapp.runMetaM x r match __discr with | (result, finalState) => pure (result, Aesop.Rapp.setMetaState finalState r)

def Aesop.RappRef.runMetaMModifying {m : Type → Type} [Monad m] [MonadLiftT Lean.MetaM m] [MonadFinally m] {α : Type} (x : m α) (rref : RappRef) : m α

Equations

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

def Aesop.Goal.runMetaMInPostNormState' {m : Type → Type} [Monad m] [MonadLiftT Lean.MetaM m] [MonadFinally m] {α : Type} [Lean.MonadError m] (x : Lean.MVarId → m α) (g : Goal) : m α

Equations

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

def Aesop.Goal.runMetaMInPostNormState {m : Type → Type} [Monad m] [MonadLiftT Lean.MetaM m] [MonadFinally m] {α : Type} [Lean.MonadError m] (x : Lean.MVarId → m α) (g : Goal) : m (α × Lean.Meta.SavedState)

Equations

• Aesop.Goal.runMetaMInPostNormState x g = Aesop.Goal.runMetaMInPostNormState' (fun (g : Lean.MVarId) => Aesop.withSaveState✝ (x g)) g

def Aesop.Goal.runMetaMInParentState' {m : Type → Type} [Monad m] [MonadLiftT Lean.MetaM m] [MonadFinally m] {α : Type} (x : m α) (g : Goal) : m α

Equations

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

def Aesop.Goal.runMetaMInParentState {m : Type → Type} [Monad m] [MonadLiftT Lean.MetaM m] [MonadFinally m] {α : Type} (x : m α) (g : Goal) : m (α × Lean.Meta.SavedState)

Equations

• Aesop.Goal.runMetaMInParentState x g = Aesop.Goal.runMetaMInParentState' (Aesop.withSaveState✝ x) g

def Aesop.Goal.runMetaMModifyingParentState {m : Type → Type} [Monad m] [MonadLiftT Lean.MetaM m] [MonadFinally m] {α : Type} (x : m α) (g : Goal) : m α

Equations

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

def Aesop.Rapp.runMetaMInParentState {m : Type → Type} [Monad m] [MonadLiftT Lean.MetaM m] [MonadFinally m] {α : Type} (x : m α) (r : Rapp) : m (α × Lean.Meta.SavedState)

Equations

• Aesop.Rapp.runMetaMInParentState x r = do let __do_lift ← ST.Ref.get r.parent Aesop.Goal.runMetaMInParentState x __do_lift

def Aesop.Rapp.runMetaMInParentState' {m : Type → Type} [Monad m] [MonadLiftT Lean.MetaM m] [MonadFinally m] {α : Type} (x : m α) (r : Rapp) : m α

Equations

• Aesop.Rapp.runMetaMInParentState' x r = do let __do_lift ← ST.Ref.get r.parent Aesop.Goal.runMetaMInParentState' x __do_lift

def Aesop.Rapp.runMetaMModifyingParentState {m : Type → Type} [Monad m] [MonadLiftT Lean.MetaM m] [MonadFinally m] {α : Type} (x : m α) (r : Rapp) : m α

Equations

• Aesop.Rapp.runMetaMModifyingParentState x r = do let __do_lift ← ST.Ref.get r.parent Aesop.Goal.runMetaMModifyingParentState x __do_lift