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.argsToMonoRedArg (args : Array (Arg Purity.pure)) (params : Array (Param Purity.pure)) (redArgs : Array (Arg Purity.pure)) :
            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.decToMono (c : Cases Purity.pure) :
                    (c.typeName == `Decidable) = true → ToMonoM (Code Purity.pure)

                    Convert cases Decidable => Bool

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