Documentation

Aesop.Builder.Unfold

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