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
        Instances For
          unsafe def Lake.OpaqueTargetConfig.unsafeMk {pkgName name : Lean.Name} :
          TargetConfig pkgName nameOpaqueTargetConfig pkgName name
          Equations
            Instances For
              instance Lake.OpaqueTargetConfig.instCoeNameTargetConfig {pkgName name : Lean.Name} :
              Coe (OpaqueTargetConfig pkgName name) (TargetConfig pkgName name)
              Equations
                instance Lake.OpaqueTargetConfig.instCoeTargetConfigName {pkgName name : Lean.Name} :
                Coe (TargetConfig pkgName name) (OpaqueTargetConfig pkgName name)
                Equations
                  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