Documentation

Aesop.Builder.Forward

source
def Aesop.RuleBuilderOptions.forwardTransparency (opts : RuleBuilderOptions) :
Lean.Meta.TransparencyMode
Instances For
    source
    def Aesop.RuleBuilderOptions.forwardIndexTransparency (opts : RuleBuilderOptions) :
    Lean.Meta.TransparencyMode
    Instances For
      source
      def Aesop.RuleBuilder.getForwardIndexingMode (type : Lean.Expr) (immediate : UnorderedArraySet PremiseIndex) :
      Lean.MetaM IndexingMode
      Instances For
        source
        def Aesop.RuleBuilder.getImmediatePremises (type : Lean.Expr) (pat? : Option RulePattern) :
        Option (Array Lean.Name) → Lean.MetaM (UnorderedArraySet PremiseIndex)
        Instances For
          source
          def Aesop.RuleBuilder.forwardCore₂ (t : ElabRuleTerm) (immediate? : Option (Array Lean.Name)) (pat? : Option RulePattern) (phase : PhaseSpec) (isDestruct : Bool) :
          Lean.MetaM ForwardRule
          Instances For
            source
            def Aesop.RuleBuilder.forwardCore (t : ElabRuleTerm) (immediate? : Option (Array Lean.Name)) (pat? : Option RulePattern) (phase : PhaseSpec) (isDestruct : Bool) :
            Lean.MetaM LocalRuleSetMember
            Instances For
              source
              def Aesop.RuleBuilder.forward (isDestruct : Bool) :
              RuleBuilder
              Instances For