Documentation

Lean.Compiler.LCNF.ToMono

source
structure Lean.Compiler.LCNF.ToMonoM.State :
Type
Instances For
    source
    @[inline, reducible]
    abbrev Lean.Compiler.LCNF.ToMonoM (α : Type) :
    Type
    Equations
    Instances For
      source
      def Lean.Compiler.LCNF.Param.toMono (param : Lean.Compiler.LCNF.Param) :
      Lean.Compiler.LCNF.ToMonoM Lean.Compiler.LCNF.Param
      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        def Lean.Compiler.LCNF.isTrivialConstructorApp? (declName : Lake.Name) (args : Array Lean.Compiler.LCNF.Arg) :
        Lean.Compiler.LCNF.ToMonoM (Option Lean.Compiler.LCNF.LetValue)
        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          def Lean.Compiler.LCNF.argToMono (arg : Lean.Compiler.LCNF.Arg) :
          Lean.Compiler.LCNF.ToMonoM Lean.Compiler.LCNF.Arg
          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            def Lean.Compiler.LCNF.ctorAppToMono (ctorInfo : Lean.ConstructorVal) (args : Array Lean.Compiler.LCNF.Arg) :
            Lean.Compiler.LCNF.ToMonoM Lean.Compiler.LCNF.LetValue
            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              partial def Lean.Compiler.LCNF.LetValue.toMono (e : Lean.Compiler.LCNF.LetValue) :
              Lean.Compiler.LCNF.ToMonoM Lean.Compiler.LCNF.LetValue
              source
              def Lean.Compiler.LCNF.LetDecl.toMono (decl : Lean.Compiler.LCNF.LetDecl) :
              Lean.Compiler.LCNF.ToMonoM Lean.Compiler.LCNF.LetDecl
              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                source
                partial def Lean.Compiler.LCNF.FunDeclCore.toMono (decl : Lean.Compiler.LCNF.FunDecl) :
                Lean.Compiler.LCNF.ToMonoM Lean.Compiler.LCNF.FunDecl
                source
                partial def Lean.Compiler.LCNF.decToMono (c : Lean.Compiler.LCNF.Cases) :
                (c.typeName == `Decidable) = true → Lean.Compiler.LCNF.ToMonoM Lean.Compiler.LCNF.Code

                Convert cases Decidable => Bool

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

                Eliminate cases for trivial structure. See hasTrivialStructure?

                source
                partial def Lean.Compiler.LCNF.Code.toMono (code : Lean.Compiler.LCNF.Code) :
                Lean.Compiler.LCNF.ToMonoM Lean.Compiler.LCNF.Code
                source
                def Lean.Compiler.LCNF.Decl.toMono (decl : Lean.Compiler.LCNF.Decl) :
                Lean.Compiler.LCNF.CompilerM Lean.Compiler.LCNF.Decl
                Equations
                Instances For
                  source
                  def Lean.Compiler.LCNF.Decl.toMono.go (decl : Lean.Compiler.LCNF.Decl) :
                  Lean.Compiler.LCNF.ToMonoM Lean.Compiler.LCNF.Decl
                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    source
                    def Lean.Compiler.LCNF.toMono :
                    Lean.Compiler.LCNF.Pass
                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For