@[reducible, inline]

abbrev Lake.ConfigType (kind pkgName name : Lean.Name) : Type

Equations

• Lake.ConfigType `lean_lib pkgName name = Lake.LeanLibConfig name
• Lake.ConfigType `lean_exe pkgName name = Lake.LeanExeConfig name
• Lake.ConfigType `extern_lib pkgName name = Lake.ExternLibConfig pkgName name
• Lake.ConfigType Lean.Name.anonymous pkgName name = Lake.OpaqueTargetConfig pkgName name
• Lake.ConfigType `input_file pkgName name = Lake.InputFileConfig name
• Lake.ConfigType `input_dir pkgName name = Lake.InputDirConfig name
• Lake.ConfigType kind pkgName name = Empty

opaque Lake.OpaqueConfigTarget (kind : Lean.Name) : Type

Forward declared ConfigTarget to work around recursion issues (e.g., with Package).

structure Lake.ConfigDecl : Type

• pkg : Lean.Name
• name : Lean.Name
• kind : Lean.Name
• config : ConfigType self.kind self.pkg self.name
• wf_data : ¬self.kind.isAnonymous = true → CustomData self.pkg self.name = DataType self.kind ∧ DataType self.kind = OpaqueConfigTarget self.kind

@[instance_reducible]

instance Lake.instTypeNameConfigDecl : TypeName ConfigDecl

Equations

• Lake.instTypeNameConfigDecl = Lake.inst✝

structure Lake.PConfigDecl (p : Lean.Name) extends Lake.ConfigDecl : Type

• pkg : Lean.Name
• name : Lean.Name
• kind : Lean.Name
• config : ConfigType self.kind self.pkg self.name
• wf_data : ¬self.kind.isAnonymous = true → CustomData self.pkg self.name = DataType self.kind ∧ DataType self.kind = OpaqueConfigTarget self.kind
• pkg_eq : self.pkg = p

structure Lake.NConfigDecl (p n : Lean.Name) extends Lake.PConfigDecl p : Type

• pkg : Lean.Name
• name : Lean.Name
• kind : Lean.Name
• config : ConfigType self.kind self.pkg self.name
• wf_data : ¬self.kind.isAnonymous = true → CustomData self.pkg self.name = DataType self.kind ∧ DataType self.kind = OpaqueConfigTarget self.kind
• pkg_eq : self.pkg = p
• name_eq : self.name = n

structure Lake.KConfigDecl (k : Lean.Name) extends Lake.ConfigDecl : Type

• pkg : Lean.Name
• name : Lean.Name
• kind : Lean.Name
• config : ConfigType self.kind self.pkg self.name
• wf_data : ¬self.kind.isAnonymous = true → CustomData self.pkg self.name = DataType self.kind ∧ DataType self.kind = OpaqueConfigTarget self.kind
• kind_eq : self.kind = k

instance Lake.instNonemptyNConfigDecl {pkg name : Lean.Name} : Nonempty (NConfigDecl pkg name)

@[inline]

def Lake.ConfigDecl.partialKey (self : ConfigDecl) : PartialBuildKey

Equations

• self.partialKey = Lake.PartialBuildKey.mk (Lake.BuildKey.packageTarget Lean.Name.anonymous self.name)

@[instance_reducible]

instance Lake.instCoeOutKConfigDeclPartialBuildKey {k : Lean.Name} : CoeOut (KConfigDecl k) PartialBuildKey

Equations

• Lake.instCoeOutKConfigDeclPartialBuildKey = { coe := fun (x : Lake.KConfigDecl k) => x.partialKey }

@[inline]

def Lake.PConfigDecl.config' {p : Lean.Name} (self : PConfigDecl p) : ConfigType self.kind p self.name

Equations

• self.config' = cast ⋯ self.config

@[inline]

def Lake.NConfigDecl.config' {p n : Lean.Name} (self : NConfigDecl p n) : ConfigType self.kind p n

Equations

• self.config' = cast ⋯ self.config'

theorem Lake.NConfigDecl.target_eq_type {p n : Lean.Name} (self : NConfigDecl p n) (h : ¬self.kind.isAnonymous = true) : DataType self.kind = OpaqueConfigTarget self.kind

theorem Lake.NConfigDecl.data_eq_target {p n : Lean.Name} (self : NConfigDecl p n) (h : ¬self.kind.isAnonymous = true) : CustomData p n = OpaqueConfigTarget self.kind

@[inline]

def Lake.ConfigDecl.config? (kind : Lean.Name) (self : ConfigDecl) : Option (ConfigType kind self.pkg self.name)

Equations

• Lake.ConfigDecl.config? kind self = if h : self.kind = kind then some (cast ⋯ self.config) else none

@[inline]

def Lake.PConfigDecl.config? {p : Lean.Name} (kind : Lean.Name) (self : PConfigDecl p) : Option (ConfigType kind p self.name)

Equations

• Lake.PConfigDecl.config? kind self = cast ⋯ (Lake.ConfigDecl.config? kind self.toConfigDecl)

@[inline]

def Lake.NConfigDecl.config? {p n : Lean.Name} (kind : Lean.Name) (self : NConfigDecl p n) : Option (ConfigType kind p n)

Equations

• Lake.NConfigDecl.config? kind self = cast ⋯ (Lake.PConfigDecl.config? kind self.toPConfigDecl)

@[inline]

def Lake.ConfigDecl.leanLibConfig? (self : ConfigDecl) : Option (LeanLibConfig self.name)

Equations

• self.leanLibConfig? = Lake.ConfigDecl.config? Lake.LeanLib.configKind self

@[inline]

def Lake.NConfigDecl.leanLibConfig? {p n : Lean.Name} (self : NConfigDecl p n) : Option (LeanLibConfig n)

Equations

• self.leanLibConfig? = Lake.NConfigDecl.config? Lake.LeanLib.configKind self

@[reducible, inline]

abbrev Lake.LeanLibDecl : Type

A Lean library declaration from a configuration written in Lean.

Equations

• Lake.LeanLibDecl = Lake.KConfigDecl Lake.LeanLib.configKind

@[inline]

def Lake.ConfigDecl.leanExeConfig? (self : ConfigDecl) : Option (LeanExeConfig self.name)

Equations

• self.leanExeConfig? = Lake.ConfigDecl.config? Lake.LeanExe.configKind self

@[inline]

def Lake.NConfigDecl.leanExeConfig? {p n : Lean.Name} (self : NConfigDecl p n) : Option (LeanExeConfig n)

Equations

• self.leanExeConfig? = Lake.NConfigDecl.config? Lake.LeanExe.configKind self

@[reducible, inline]

abbrev Lake.LeanExeDecl : Type

A Lean executable declaration from a configuration written in Lean.

Equations

• Lake.LeanExeDecl = Lake.KConfigDecl Lake.LeanExe.configKind

@[inline]

def Lake.PConfigDecl.externLibConfig? {p : Lean.Name} (self : PConfigDecl p) : Option (ExternLibConfig p self.name)

Equations

• self.externLibConfig? = Lake.PConfigDecl.config? Lake.ExternLib.configKind self

@[inline]

def Lake.NConfigDecl.externLibConfig? {p n : Lean.Name} (self : NConfigDecl p n) : Option (ExternLibConfig p n)

Equations

• self.externLibConfig? = Lake.NConfigDecl.config? Lake.ExternLib.configKind self

@[reducible, inline]

abbrev Lake.ExternLibDecl : Type

An external library declaration from a configuration written in Lean.

Equations

• Lake.ExternLibDecl = Lake.KConfigDecl Lake.ExternLib.configKind

@[inline]

def Lake.PConfigDecl.opaqueTargetConfig {p : Lean.Name} (self : PConfigDecl p) (h : self.kind.isAnonymous = true) : OpaqueTargetConfig p self.name

Equations

• self.opaqueTargetConfig h = cast ⋯ self.config

@[inline]

def Lake.NConfigDecl.opaqueTargetConfig {p n : Lean.Name} (self : NConfigDecl p n) (h : self.kind.isAnonymous = true) : OpaqueTargetConfig p n

Equations

• self.opaqueTargetConfig h = cast ⋯ (self.opaqueTargetConfig h)

@[inline]

def Lake.PConfigDecl.opaqueTargetConfig? {p : Lean.Name} (self : PConfigDecl p) : Option (OpaqueTargetConfig p self.name)

Equations

• self.opaqueTargetConfig? = if h : self.kind.isAnonymous = true then some (self.opaqueTargetConfig h) else none

@[inline]

def Lake.NConfigDecl.opaqueTargetConfig? {p n : Lean.Name} (self : NConfigDecl p n) : Option (OpaqueTargetConfig p n)

Equations

• self.opaqueTargetConfig? = cast ⋯ self.opaqueTargetConfig?

@[reducible, inline]

abbrev Lake.InputFileDecl : Type

An input file declaration from a configuration written in Lean.

Equations

• Lake.InputFileDecl = Lake.KConfigDecl Lake.InputFile.configKind

@[reducible, inline]

abbrev Lake.InputDirDecl : Type

An input directory declaration from a configuration written in Lean.

Equations

• Lake.InputDirDecl = Lake.KConfigDecl Lake.InputDir.configKind

@[instance_reducible]

instance Lake.instTypeNameLeanLibDecl : TypeName LeanLibDecl

Equations

• Lake.instTypeNameLeanLibDecl = Lake.instTypeNameLeanLibDecl.unsafe_impl_2

@[instance_reducible]

instance Lake.instTypeNameLeanExeDecl : TypeName LeanExeDecl

Equations

• Lake.instTypeNameLeanExeDecl = Lake.instTypeNameLeanExeDecl.unsafe_impl_2

@[instance_reducible]

instance Lake.instTypeNameInputFileDecl : TypeName InputFileDecl

Equations

• Lake.instTypeNameInputFileDecl = Lake.instTypeNameInputFileDecl.unsafe_impl_2

@[instance_reducible]

instance Lake.instTypeNameInputDirDecl : TypeName InputDirDecl

Equations

• Lake.instTypeNameInputDirDecl = Lake.instTypeNameInputDirDecl.unsafe_impl_2