Documentation

Lean.Compiler.LCNF.ToMono

source
structure Lean.Compiler.LCNF.ToMonoM.State :
Type
Instances For
    source
    @[reducible, inline]
    abbrev Lean.Compiler.LCNF.ToMonoM (α : Type) :
    Type
    Instances For
      source
      def Lean.Compiler.LCNF.Param.toMono (param : Param Purity.pure) :
      ToMonoM (Param Purity.pure)
      Instances For
        source
        @[inline]
        def Lean.Compiler.LCNF.argToMono (arg : Arg Purity.pure) :
        ToMonoM (Arg Purity.pure)
        Instances For
          source
          def Lean.Compiler.LCNF.argsToMonoWithFnType (args : Array (Arg Purity.pure)) (type : Expr) :
          ToMonoM (Array (Arg Purity.pure))
          Instances For
            source
            def Lean.Compiler.LCNF.ctorAppToMono (ctorInfo : ConstructorVal) (args : Array (Arg Purity.pure)) :
            ToMonoM (LetValue Purity.pure)
            Instances For
              source
              partial def Lean.Compiler.LCNF.LetValue.toMono (e : LetValue Purity.pure) :
              ToMonoM (LetValue Purity.pure)
              source
              def Lean.Compiler.LCNF.LetDecl.toMono (decl : LetDecl Purity.pure) :
              ToMonoM (LetDecl Purity.pure)
              Instances For
                source
                def Lean.Compiler.LCNF.mkFieldParamsForComputedFields (ctorType : Expr) (numParams numNewFields : Nat) (oldFields : Array (Param Purity.pure)) :
                ToMonoM (Array (Param Purity.pure))
                Instances For
                  source
                  partial def Lean.Compiler.LCNF.FunDecl.toMono (decl : FunDecl Purity.pure) :
                  ToMonoM (FunDecl Purity.pure)
                  source
                  partial def Lean.Compiler.LCNF.casesNatToMono (c : Cases Purity.pure) :
                  (c.typeName == `Nat) = true → ToMonoM (Code Purity.pure)

                  Eliminate cases for Nat.

                  source
                  partial def Lean.Compiler.LCNF.casesIntToMono (c : Cases Purity.pure) :
                  (c.typeName == `Int) = true → ToMonoM (Code Purity.pure)

                  Eliminate cases for Int.

                  source
                  partial def Lean.Compiler.LCNF.casesUIntToMono (c : Cases Purity.pure) (uintName : Name) :
                  (c.typeName == uintName) = true → ToMonoM (Code Purity.pure)

                  Eliminate cases for UInt types.

                  source
                  partial def Lean.Compiler.LCNF.casesArrayToMono (c : Cases Purity.pure) :
                  (c.typeName == `Array) = true → ToMonoM (Code Purity.pure)

                  Eliminate cases for `Array.

                  source
                  partial def Lean.Compiler.LCNF.casesByteArrayToMono (c : Cases Purity.pure) :
                  (c.typeName == `ByteArray) = true → ToMonoM (Code Purity.pure)

                  Eliminate cases for `ByteArray.

                  source
                  partial def Lean.Compiler.LCNF.casesFloatArrayToMono (c : Cases Purity.pure) :
                  (c.typeName == `FloatArray) = true → ToMonoM (Code Purity.pure)

                  Eliminate cases for `FloatArray.

                  source
                  partial def Lean.Compiler.LCNF.casesStringToMono (c : Cases Purity.pure) :
                  (c.typeName == `String) = true → ToMonoM (Code Purity.pure)

                  Eliminate cases for String.

                  source
                  partial def Lean.Compiler.LCNF.casesFloatToMono (c : Cases Purity.pure) :
                  (c.typeName == `Float) = true → ToMonoM (Code Purity.pure)

                  Eliminate cases for Float.

                  source
                  partial def Lean.Compiler.LCNF.casesFloat32ToMono (c : Cases Purity.pure) :
                  (c.typeName == `Float32) = true → ToMonoM (Code Purity.pure)

                  Eliminate cases for Float32.

                  source
                  partial def Lean.Compiler.LCNF.casesThunkToMono (c : Cases Purity.pure) :
                  (c.typeName == `Thunk) = true → ToMonoM (Code Purity.pure)

                  Eliminate cases for `Thunk.

                  source
                  partial def Lean.Compiler.LCNF.casesTaskToMono (c : Cases Purity.pure) :
                  (c.typeName == `Task) = true → ToMonoM (Code Purity.pure)

                  Eliminate cases for `Task.

                  source
                  partial def Lean.Compiler.LCNF.trivialStructToMono (info : TrivialStructureInfo) (c : Cases Purity.pure) :
                  ToMonoM (Code Purity.pure)

                  Eliminate cases for trivial structure. See hasTrivialStructure?

                  source
                  partial def Lean.Compiler.LCNF.Code.toMono (code : Code Purity.pure) :
                  ToMonoM (Code Purity.pure)
                  source
                  def Lean.Compiler.LCNF.Decl.toMono (decl : Decl Purity.pure) :
                  CompilerM (Decl Purity.pure)
                  Instances For
                    source
                    def Lean.Compiler.LCNF.toMono :
                    Pass
                    Instances For