Documentation

Aesop.Builder.Unfold

source
def Aesop.RuleBuilder.hasConst (c : Lean.Name) (e : Lean.Expr) :
Bool
Equations
    Instances For
      source
      def Aesop.RuleBuilder.checkUnfoldableConst (decl : Lean.Name) :
      Lean.MetaM (Option Lean.Name)
      Equations
        Instances For
          source
          def Aesop.RuleBuilder.unfoldCore (decl : Lean.Name) :
          Lean.MetaM LocalRuleSetMember
          Equations
            Instances For
              source
              def Aesop.RuleBuilder.unfold :
              RuleBuilder
              Equations
                Instances For