Documentation

Lean.Compiler.LCNF.ToMono

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
        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
            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              def Lean.Compiler.LCNF.argsToMonoRedArg (resultFVar : FVarId) (args : Array Arg) (params : Array Param) (redArgs : Array Arg) :
              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
                  Equations
                  Instances For
                    def Lean.Compiler.LCNF.mkFieldParamsForComputedFields (ctorType : Expr) (numParams numNewFields : Nat) (oldFields : Array Param) :
                    Equations
                    • One or more equations did not get rendered due to their size.
                    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 `Thunk.

                      Eliminate cases for `Task.

                      Eliminate cases for trivial structure. See hasTrivialStructure?

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