Documentation

Aesop.Builder.Apply

source
def Aesop.RuleBuilderOptions.applyTransparency (opts : RuleBuilderOptions) :
Lean.Meta.TransparencyMode
Equations
    Instances For
      source
      def Aesop.RuleBuilderOptions.applyIndexTransparency (opts : RuleBuilderOptions) :
      Lean.Meta.TransparencyMode
      Equations
        Instances For
          source
          def Aesop.RuleBuilder.getApplyIndexingMode (indexMd : Lean.Meta.TransparencyMode) (type : Lean.Expr) :
          Lean.MetaM IndexingMode
          Equations
            Instances For
              source
              def Aesop.RuleBuilder.checkNoIff (type : Lean.Expr) :
              Lean.MetaM Unit
              Equations
                Instances For
                  source
                  def Aesop.RuleBuilder.applyCore (t : ElabRuleTerm) (pat? : Option RulePattern) (imode? : Option IndexingMode) (md indexMd : Lean.Meta.TransparencyMode) (phase : PhaseSpec) :
                  Lean.MetaM LocalRuleSetMember
                  Equations
                    Instances For
                      source
                      def Aesop.RuleBuilder.apply :
                      RuleBuilder
                      Equations
                        Instances For