Documentation

Lean.Compiler.LCNF.Simp.DiscrM

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
        Instances For
          @[inline, reducible]

          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
                  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