Documentation

Aesop.RPINF

source
def Aesop.instMonadCacheExprBaseM :
Lean.MonadCache Lean.Expr Lean.Expr BaseM
Equations
    Instances For
      source
      @[specialize #[]]
      def Aesop.rpinfRaw (e : Lean.Expr) :
      BaseM RPINFRaw
      Equations
        Instances For
          source
          partial def Aesop.rpinfRaw.go (e : Lean.Expr) :
          BaseM Lean.Expr
          source
          partial def Aesop.rpinfRaw.withNewFVars {α : Type} (fvars : Array Lean.Expr) (k : BaseM α) :
          BaseM α
          source
          def Aesop.rpinf (e : Lean.Expr) :
          BaseM RPINF
          Equations
            Instances For