Documentation

Lean.Compiler.LCNF.StructProjCases

source
def Lean.Compiler.LCNF.StructProjCases.findStructCtorInfo? (typeName : Name) :
CoreM (Option ConstructorVal)
Instances For
    source
    def Lean.Compiler.LCNF.StructProjCases.mkFieldParamsForCtorType (ctorType : Expr) (numParams numFields : Nat) :
    CompilerM (Array (Param Purity.pure))
    Instances For
      source
      structure Lean.Compiler.LCNF.StructProjCases.State :
      Type
      Instances For
        source
        @[reducible, inline]
        abbrev Lean.Compiler.LCNF.StructProjCases.M (α : Type) :
        Type
        Instances For
          source
          def Lean.Compiler.LCNF.StructProjCases.M.run {α : Type} (x : M α) :
          CompilerM α
          Instances For
            source
            def Lean.Compiler.LCNF.StructProjCases.remapFVar (fvarId : FVarId) :
            M FVarId
            Instances For
              source
              partial def Lean.Compiler.LCNF.StructProjCases.visitCode (code : Code Purity.pure) :
              M (Code Purity.pure)
              source
              def Lean.Compiler.LCNF.StructProjCases.visitLetValue (v : LetValue Purity.pure) :
              M (LetValue Purity.pure)
              Instances For
                source
                partial def Lean.Compiler.LCNF.StructProjCases.visitAlt (alt : Alt Purity.pure) :
                M (Alt Purity.pure)
                source
                def Lean.Compiler.LCNF.StructProjCases.visitArg (arg : Arg Purity.pure) :
                M (Arg Purity.pure)
                Instances For
                  source
                  def Lean.Compiler.LCNF.StructProjCases.visitDecl (decl : Decl Purity.pure) :
                  M (Decl Purity.pure)
                  Instances For
                    source
                    def Lean.Compiler.LCNF.structProjCases :
                    Pass
                    Instances For