Documentation

Lean.Compiler.IR.ToIR

source
structure Lean.IR.ToIR.BuilderState :
Type
Instances For
    source
    @[reducible, inline]
    abbrev Lean.IR.ToIR.M (α : Type) :
    Type
    Instances For
      source
      def Lean.IR.ToIR.M.run {α : Type} (x : M α) :
      CoreM α
      Instances For
        source
        def Lean.IR.ToIR.getFVarValue (fvarId : FVarId) :
        M Arg
        Instances For
          source
          def Lean.IR.ToIR.getJoinPointValue (fvarId : FVarId) :
          M JoinPointId
          Instances For
            source
            def Lean.IR.ToIR.bindVar (fvarId : FVarId) :
            M VarId
            Instances For
              source
              def Lean.IR.ToIR.bindJoinPoint (fvarId : FVarId) :
              M JoinPointId
              Instances For
                source
                def Lean.IR.ToIR.bindErased (fvarId : FVarId) :
                M Unit
                Instances For
                  source
                  def Lean.IR.ToIR.addDecl (d : Decl) :
                  M Unit
                  Instances For
                    source
                    def Lean.IR.ToIR.lowerLitValue (v : Compiler.LCNF.LitValue) :
                    LitVal × IRType
                    Instances For
                      source
                      def Lean.IR.ToIR.lowerArg (a : Compiler.LCNF.Arg Compiler.LCNF.Purity.impure) :
                      M Arg
                      Instances For
                        source
                        def Lean.IR.ToIR.lowerParam (p : Compiler.LCNF.Param Compiler.LCNF.Purity.impure) :
                        M Param
                        Instances For
                          source
                          @[inline]
                          def Lean.IR.ToIR.lowerCtorInfo (i : Compiler.LCNF.CtorInfo) :
                          CtorInfo
                          Instances For
                            source
                            partial def Lean.IR.ToIR.lowerCode (c : Compiler.LCNF.Code Compiler.LCNF.Purity.impure) :
                            M FnBody
                            source
                            partial def Lean.IR.ToIR.lowerLet (decl : Compiler.LCNF.LetDecl Compiler.LCNF.Purity.impure) (k : Compiler.LCNF.Code Compiler.LCNF.Purity.impure) :
                            M FnBody
                            source
                            partial def Lean.IR.ToIR.lowerAlt (a : Compiler.LCNF.Alt Compiler.LCNF.Purity.impure) :
                            M Alt
                            source
                            def Lean.IR.ToIR.lowerDecl (d : Compiler.LCNF.Decl Compiler.LCNF.Purity.impure) :
                            M (Option Decl)
                            Instances For
                              source
                              def Lean.IR.toIR (decls : Array (Compiler.LCNF.Decl Compiler.LCNF.Purity.impure)) :
                              CoreM (Array Decl)
                              Instances For