Documentation

Lean.Compiler.LCNF.Simp.DiscrM

Instances For
    Instances For
      @[reducible, inline]

      Helper monad for tracking mappings from discriminant to constructor applications and back. The combinator withDiscrCtor should be used when visiting cases alternatives.

      Equations
      Instances For

        If fvarId is a constructor application, returns constructor information. Remark: we use the map discrCtorMap. Remark: We use this method when simplifying projections and cases-constructor.

        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

            If type is an inductive datatype, return its universe levels and parameters.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              @[inline]

              Execute x with the information that discr = ctorName ctorFields. We use this information to simplify nested cases on the same discriminant.

              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
                  @[inline]

                  Execute x with the information that discr = ctorName ctorFields. We use this information to simplify nested cases on the same discriminant.

                  Equations
                  Instances For
                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For