Documentation

Lean.Meta.Match.MatcherInfo

  • hName? : Option Name

    some h if the discriminant is annotated with h:

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
        Instances For
          Equations
            Instances For
              Instances For
                Equations
                  Instances For
                    Equations
                      Instances For
                        def Lean.Meta.Match.addMatcherInfo {m : TypeType} [Monad m] [MonadEnv m] (matcherName : Name) (info : MatcherInfo) :
                        Equations
                          Instances For
                            Equations
                              Instances For
                                def Lean.Meta.getMatcherInfo? {m : TypeType} [Monad m] [MonadEnv m] (declName : Name) :
                                Equations
                                  Instances For
                                    @[export lean_is_matcher]
                                    def Lean.Meta.isMatcherCore (env : Environment) (declName : Name) :
                                    Equations
                                      Instances For
                                        def Lean.Meta.isMatcher {m : TypeType} [Monad m] [MonadEnv m] (declName : Name) :
                                        Equations
                                          Instances For
                                            Equations
                                              Instances For
                                                Equations
                                                  Instances For
                                                    def Lean.Meta.isMatcherApp {m : TypeType} [Monad m] [MonadEnv m] (e : Expr) :
                                                    Equations
                                                      Instances For