def Aesop.Rapp.runMetaM {α : Type} (x : Lean.MetaM α) (r : Aesop.Rapp) : Lean.MetaM (α × Lean.Meta.SavedState)

Equations

• Aesop.Rapp.runMetaM x r = Lean.Meta.SavedState.runMetaM (Aesop.Rapp.metaState r) x

def Aesop.Rapp.runMetaM' {α : Type} (x : Lean.MetaM α) (r : Aesop.Rapp) : Lean.MetaM α

Equations

• Aesop.Rapp.runMetaM' x r = Prod.fst <$> Aesop.Rapp.runMetaM x r

def Aesop.Rapp.runMetaMModifying {α : Type} (x : Lean.MetaM α) (r : Aesop.Rapp) : Lean.MetaM (α × Aesop.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 {α : Type} (x : Lean.MetaM α) (rref : Aesop.RappRef) : Lean.MetaM α

Equations

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

def Aesop.Goal.runMetaMInPostNormState {α : Type} (x : Lean.MVarId → Lean.MetaM α) (g : Aesop.Goal) : Lean.MetaM (α × Lean.Meta.SavedState)

Equations

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

def Aesop.Goal.runMetaMInPostNormState' {α : Type} (x : Lean.MVarId → Lean.MetaM α) (g : Aesop.Goal) : Lean.MetaM α

Equations

• Aesop.Goal.runMetaMInPostNormState' x g = Prod.fst <$> Aesop.Goal.runMetaMInPostNormState x g

def Aesop.Goal.runMetaMInParentState {α : Type} (x : Lean.MetaM α) (g : Aesop.Goal) : Lean.MetaM (α × Lean.Meta.SavedState)

Equations

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

def Aesop.Goal.runMetaMInParentState' {α : Type} (x : Lean.MetaM α) (g : Aesop.Goal) : Lean.MetaM α

Equations

• Aesop.Goal.runMetaMInParentState' x g = Prod.fst <$> Aesop.Goal.runMetaMInParentState x g

def Aesop.Goal.runMetaMModifyingParentState {α : Type} (x : Lean.MetaM α) (g : Aesop.Goal) : Lean.MetaM α

Equations

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

def Aesop.Rapp.runMetaMInParentState {α : Type} (x : Lean.MetaM α) (r : Aesop.Rapp) : Lean.MetaM (α × Lean.Meta.SavedState)

Equations

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

def Aesop.Rapp.runMetaMInParentState' {α : Type} (x : Lean.MetaM α) (r : Aesop.Rapp) : Lean.MetaM α

Equations

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

def Aesop.Rapp.runMetaMModifyingParentState {α : Type} (x : Lean.MetaM α) (r : Aesop.Rapp) : Lean.MetaM α

Equations

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