Documentation

Lean.Meta.Match.NamedPatterns

Helper functions around named patterns

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