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

Equations

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

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

Equations

• Aesop.Goal.runMetaMModifyingParentState x g = do let __do_lift ← liftM g.parentRapp? match __do_lift with | none => x | some rref => Aesop.RappRef.runMetaMModifying x rref

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

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 {α : Type} (x : Lean.MetaM α) (r : Rapp) : Lean.MetaM α

Equations

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