Documentation

Aesop.Builder.Constructors

source
def Aesop.RuleBuilderOptions.constructorsTransparency (opts : RuleBuilderOptions) :
Lean.Meta.TransparencyMode
Instances For
    source
    def Aesop.RuleBuilderOptions.constructorsIndexTransparency (opts : RuleBuilderOptions) :
    Lean.Meta.TransparencyMode
    Instances For
      source
      def Aesop.RuleBuilder.getConstructorsIndexingMode (indexMd : Lean.Meta.TransparencyMode) (info : Lean.InductiveVal) :
      Lean.MetaM IndexingMode
      Instances For
        source
        def Aesop.RuleBuilder.constructorsCore (info : Lean.InductiveVal) (imode? : Option IndexingMode) (md indexMd : Lean.Meta.TransparencyMode) (phase : PhaseSpec) :
        Lean.MetaM LocalRuleSetMember
        Instances For
          source
          def Aesop.RuleBuilder.constructors :
          RuleBuilder
          Instances For