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 }

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

Equations

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