Documentation

Lean.Meta.Match.MatcherInfo

Instances For

    A "matcher" auxiliary declaration has the following structure:

    • numParams parameters
    • motive
    • numDiscrs discriminators (aka major premises)
    • altNumParams.size alternatives (aka minor premises) where alternative i has altNumParams[i] parameters
    • uElimPos? is some pos when the matcher can eliminate in different universe levels, and pos is the position of the universe level parameter that specifies the elimination universe. It is none if the matcher only eliminates into Prop.
    Instances For
      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        Equations
        Instances For
          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              Equations
              • One or more equations did not get rendered due to their size.
              Equations
              Instances For
                @[export lean_is_matcher]
                Equations
                Instances For
                  def Lean.Meta.isMatcher {m : TypeType} [Monad m] [Lean.MonadEnv m] (declName : Lake.Name) :
                  Equations
                  Instances For
                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For
                      Equations
                      Instances For
                        Instances For
                          Equations
                          • One or more equations did not get rendered due to their size.
                          Instances For
                            Equations
                            • One or more equations did not get rendered due to their size.
                            Instances For