Documentation

Lean.Meta.MatchUtil

source
@[inline]
def Lean.Meta.testHelper (e : Lean.Expr) (p : Lean.Expr → Lean.MetaM Bool) :
Lean.MetaM Bool
Instances For
    source
    @[inline]
    def Lean.Meta.matchHelper? {α : Type} (e : Lean.Expr) (p? : Lean.Expr → Lean.MetaM (Option α)) :
    Lean.MetaM (Option α)
    Instances For
      source
      def Lean.Meta.matchEq? (e : Lean.Expr) :
      Lean.MetaM (Option (Lean.Expr × Lean.Expr × Lean.Expr))

      Matches e with lhs = (rhs : α) and returns (α, lhs, rhs).

      Instances For
        source
        def Lean.Meta.matchHEq? (e : Lean.Expr) :
        Lean.MetaM (Option (Lean.Expr × Lean.Expr × Lean.Expr × Lean.Expr))
        Instances For
          source
          def Lean.Meta.matchEqHEq? (e : Lean.Expr) :
          Lean.MetaM (Option (Lean.Expr × Lean.Expr × Lean.Expr))

          Return some (α, lhs, rhs) if e is of the form @Eq α lhs rhs or @HEq α lhs α rhs

          Instances For
            source
            def Lean.Meta.matchFalse (e : Lean.Expr) :
            Lean.MetaM Bool
            Instances For
              source
              def Lean.Meta.matchNot? (e : Lean.Expr) :
              Lean.MetaM (Option Lean.Expr)
              Instances For
                source
                def Lean.Meta.matchNe? (e : Lean.Expr) :
                Lean.MetaM (Option (Lean.Expr × Lean.Expr × Lean.Expr))
                Instances For
                  source
                  def Lean.Meta.matchConstructorApp? (e : Lean.Expr) :
                  Lean.MetaM (Option Lean.ConstructorVal)
                  Instances For