def Aesop.instMonadCacheExprBaseM : Lean.MonadCache Lean.Expr Lean.Expr BaseM

Equations

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

@[specialize #[]]

def Aesop.rpinfRaw (e : Lean.Expr) : BaseM RPINFRaw

Equations

• Aesop.rpinfRaw e = Lean.Meta.withReducible do let __do_lift ← Aesop.rpinfRaw.go e pure { toExpr := __do_lift }

partial def Aesop.rpinfRaw.go (e : Lean.Expr) : BaseM Lean.Expr

partial def Aesop.rpinfRaw.withNewFVars {α : Type} (fvars : Array Lean.Expr) (k : BaseM α) : BaseM α

def Aesop.rpinf (e : Lean.Expr) : BaseM RPINF

Equations

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