Documentation

Lean.Compiler.LCNF.ToMono

Instances For
    @[reducible, inline]
    Equations
      Instances For
        Equations
          Instances For
            Equations
              Instances For
                Equations
                  Instances For
                    Equations
                      Instances For
                        Equations
                          Instances For
                            partial def Lean.Compiler.LCNF.decToMono (c : Cases) :
                            (c.typeName == `Decidable) = trueToMonoM Code

                            Convert cases Decidable => Bool

                            Eliminate cases for Nat.

                            Eliminate cases for Int.

                            partial def Lean.Compiler.LCNF.casesUIntToMono (c : Cases) (uintName : Name) :
                            (c.typeName == uintName) = trueToMonoM Code

                            Eliminate cases for UInt types.

                            Eliminate cases for `Array.

                            Eliminate cases for `ByteArray.

                            Eliminate cases for `FloatArray.

                            Eliminate cases for `String.

                            Eliminate cases for trivial structure. See hasTrivialStructure?

                            Equations
                              Instances For
                                Equations
                                  Instances For
                                    Equations
                                      Instances For