Documentation

Lean.Meta.Match.MatcherApp.Basic

Instances For
    def Lean.Meta.matchMatcherApp? {m : TypeType} [Monad m] [MonadEnv m] [MonadError m] (e : Expr) (alsoCasesOn : Bool := false) :

    Recognizes if e is a matcher application, and destructs it into the MatcherApp data structure.

    This can optionally also treat casesOn recursor applications as a special case of matcher applications.

    Equations
      Instances For
        Equations
          Instances For