Documentation

Lake.Config.TargetConfig

structure Lake.TargetConfig (pkgName name : Lean.Name) :

A custom target's declarative configuration.

Instances For
    Equations
    Instances For
      @[inline]
      def Lake.mkTargetJobConfig {α : Type} {pkgName name : Lean.Name} [FormatQuery α] [h : FamilyOut (CustomData pkgName) name α] (fetch : NPackage pkgNameFetchM (Job α)) :
      TargetConfig pkgName name

      A smart constructor for target configurations that generate CLI targets.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        @[implemented_by _private.Lake.Config.TargetConfig.0.Lake.OpaqueTargetConfig.unsafeMk]
        opaque Lake.OpaqueTargetConfig.mk {pkgName name : Lean.Name} :
        TargetConfig pkgName nameOpaqueTargetConfig pkgName name
        @[implemented_by _private.Lake.Config.TargetConfig.0.Lake.OpaqueTargetConfig.unsafeGet]
        opaque Lake.OpaqueTargetConfig.get {pkgName name : Lean.Name} :
        OpaqueTargetConfig pkgName nameTargetConfig pkgName name
        @[inline]
        Equations
        Instances For
          @[inline]
          Equations
          Instances For
            @[reducible, inline]

            A dependently typed configuration based on its registered package and name.

            Equations
            Instances For

              Try to find a target configuration in the package with the given name .

              Equations
              Instances For