Documentation

Lake.Config.TargetConfig

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

A custom target's declarative configuration.

Instances For
    instance Lake.instInhabitedTargetConfig {a✝ a✝¹ : Lean.Name} :
    Inhabited (TargetConfig a✝ a✝¹)
    Equations
    @[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
      unsafe def Lake.OpaqueTargetConfig.unsafeMk {pkgName name : Lean.Name} :
      TargetConfig pkgName nameOpaqueTargetConfig pkgName name
      Equations
      Instances For
        unsafe def Lake.OpaqueTargetConfig.unsafeGet {pkgName name : Lean.Name} :
        OpaqueTargetConfig pkgName nameTargetConfig pkgName name
        Equations
        Instances For
          @[implemented_by Lake.OpaqueTargetConfig.unsafeMk]
          opaque Lake.OpaqueTargetConfig.mk {pkgName name : Lean.Name} :
          TargetConfig pkgName nameOpaqueTargetConfig pkgName name
          @[implemented_by 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