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
      • info.numAlts = info.altNumParams.size
      Instances For
        Equations
        • info.arity = info.numParams + 1 + info.numDiscrs + info.numAlts
        Instances For
          Equations
          • info.getFirstDiscrPos = info.numParams + 1
          Instances For
            Equations
            • info.getDiscrRange = { start := info.getFirstDiscrPos, stop := info.getFirstDiscrPos + info.numDiscrs, step := 1 }
            Instances For
              Equations
              • info.getFirstAltPos = info.numParams + 1 + info.numDiscrs
              Instances For
                Equations
                • info.getAltRange = { start := info.getFirstAltPos, stop := info.getFirstAltPos + info.numAlts, step := 1 }
                Instances For
                  Equations
                  • info.getMotivePos = info.numParams
                  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.
                        Equations
                        Instances For
                          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