Documentation

Lean.Meta.Match.NamedPatterns

Helper functions around named patterns

source
def Lean.Meta.Match.mkNamedPattern (x h p : Expr) :
MetaM Expr
Equations
    Instances For
      source
      def Lean.Meta.Match.isNamedPattern (e : Expr) :
      Bool
      Equations
        Instances For
          source
          def Lean.Meta.Match.isNamedPattern? (e : Expr) :
          Option Expr
          Equations
            Instances For
              source
              def Lean.Meta.Match.unfoldNamedPattern (e : Expr) :
              MetaM Expr
              Equations
                Instances For