Documentation

Lean.Compiler.LCNF.ToExpr

source
@[reducible, inline]
abbrev Lean.Compiler.LCNF.ToExpr.LevelMap :
Type
Instances For
    source
    @[reducible, inline]
    abbrev Lean.Compiler.LCNF.ToExpr.ToExprM (α : Type) :
    Type
    Instances For
      source
      @[inline]
      def Lean.Compiler.LCNF.ToExpr.mkLambdaM {pu : Purity} (params : Array (Param pu)) (e : Expr) :
      ToExprM Expr
      Instances For
        source
        @[inline]
        def Lean.Compiler.LCNF.ToExpr.abstractM (e : Expr) :
        ToExprM Expr
        Instances For
          source
          @[inline]
          def Lean.Compiler.LCNF.ToExpr.withFVar {α : Type} (fvarId : FVarId) (k : ToExprM α) :
          ToExprM α
          Instances For
            source
            @[inline]
            def Lean.Compiler.LCNF.ToExpr.withParams {pu : Purity} {α : Type} (params : Array (Param pu)) (k : ToExprM α) :
            ToExprM α
            Instances For
              source
              @[inline]
              def Lean.Compiler.LCNF.ToExpr.run {α : Type} (x : ToExprM α) (offset : Nat := 0) (levelMap : LevelMap := ∅) :
              α
              Instances For
                source
                @[inline]
                def Lean.Compiler.LCNF.ToExpr.run' {α : Type} (x : ToExprM α) (xs : Array FVarId) :
                α
                Instances For
                  source
                  partial def Lean.Compiler.LCNF.FunDecl.toExprM {pu : Purity} (decl : FunDecl pu) :
                  ToExpr.ToExprM Expr
                  source
                  partial def Lean.Compiler.LCNF.Code.toExprM {pu : Purity} (code : Code pu) :
                  ToExpr.ToExprM Expr
                  source
                  def Lean.Compiler.LCNF.Code.toExpr {pu : Purity} (code : Code pu) (xs : Array FVarId := #[]) :
                  Expr
                  Instances For
                    source
                    def Lean.Compiler.LCNF.FunDecl.toExpr {pu : Purity} (decl : FunDecl pu) (xs : Array FVarId := #[]) :
                    Expr
                    Instances For