@[reducible, inline]

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

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 Lake.instTypeNameConfigDecl : TypeName ConfigDecl

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

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

@[inline]

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

@[inline]

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

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)

@[inline]

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

@[inline]

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

@[inline]

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

@[inline]

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

@[reducible, inline]

abbrev Lake.LeanLibDecl : Type

A Lean library declaration from a configuration written in Lean.

@[inline]

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

@[inline]

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

@[reducible, inline]

abbrev Lake.LeanExeDecl : Type

A Lean executable declaration from a configuration written in Lean.

@[inline]

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

@[inline]

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

@[reducible, inline]

abbrev Lake.ExternLibDecl : Type

An external library declaration from a configuration written in Lean.

@[inline]

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

@[inline]

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

@[inline]

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

@[inline]

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

@[reducible, inline]

abbrev Lake.InputFileDecl : Type

A input file declaration from a configuration written in Lean.

@[reducible, inline]

abbrev Lake.InputDirDecl : Type

A inpurt directory declaration from a configuration written in Lean.

instance Lake.instTypeNameLeanExeDecl : TypeName LeanExeDecl

instance Lake.instTypeNameLeanLibDecl : TypeName LeanLibDecl

instance Lake.instTypeNameInputFileDecl : TypeName InputFileDecl

instance Lake.instTypeNameInputDirDecl : TypeName InputDirDecl