Lake.Config.ConfigDecl

source

@[reducible, inline]

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

Type

Instances For

source

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

Type

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

source

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

Instances For

source

@[implicit_reducible]

instance Lake.instTypeNameConfigDecl :

TypeName ConfigDecl

source

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

Instances For

source

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

Instances For

source

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

Instances For

source

instance Lake.instNonemptyNConfigDecl {pkg name : Lean.Name} :

Nonempty (NConfigDecl pkg name)

source

@[inline]

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

PartialBuildKey

Instances For

source

@[implicit_reducible]

instance Lake.instCoeOutKConfigDeclPartialBuildKey {k : Lean.Name} :

CoeOut (KConfigDecl k) PartialBuildKey

source

@[inline]

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

ConfigType self.kind p self.name

Instances For

source

@[inline]

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

ConfigType self.kind p n

Instances For

source

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

source

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

source

@[inline]

def Lake.ConfigDecl.config? (kind : Lean.Name) (self : ConfigDecl) :

Option (ConfigType kind self.pkg self.name)

Instances For

source

@[inline]

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

Option (ConfigType kind p self.name)

Instances For

source

@[inline]

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

Option (ConfigType kind p n)

Instances For

source

@[inline]

def Lake.ConfigDecl.leanLibConfig? (self : ConfigDecl) :

Option (LeanLibConfig self.name)

Instances For

source

@[inline]

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

Option (LeanLibConfig n)

Instances For

source

@[reducible, inline]

abbrev Lake.LeanLibDecl :

Type

A Lean library declaration from a configuration written in Lean.

Instances For

source

@[inline]

def Lake.ConfigDecl.leanExeConfig? (self : ConfigDecl) :

Option (LeanExeConfig self.name)

Instances For

source

@[inline]

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

Option (LeanExeConfig n)

Instances For

source

@[reducible, inline]

abbrev Lake.LeanExeDecl :

Type

A Lean executable declaration from a configuration written in Lean.

Instances For

source

@[inline]

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

Option (ExternLibConfig p self.name)

Instances For

source

@[inline]

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

Option (ExternLibConfig p n)

Instances For

source

@[reducible, inline]

abbrev Lake.ExternLibDecl :

Type

An external library declaration from a configuration written in Lean.

Instances For

source

@[inline]

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

OpaqueTargetConfig p self.name

Instances For

source

@[inline]

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

OpaqueTargetConfig p n

Instances For

source

@[inline]

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

Option (OpaqueTargetConfig p self.name)

Instances For

source

@[inline]

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

Option (OpaqueTargetConfig p n)

Instances For

source

@[reducible, inline]

abbrev Lake.InputFileDecl :

Type

An input file declaration from a configuration written in Lean.

Instances For

source

@[reducible, inline]

abbrev Lake.InputDirDecl :

Type

An input directory declaration from a configuration written in Lean.

Instances For

source

@[implicit_reducible]

instance Lake.instTypeNameLeanLibDecl :

TypeName LeanLibDecl

source

@[implicit_reducible]

instance Lake.instTypeNameLeanExeDecl :

TypeName LeanExeDecl

source

@[implicit_reducible]

instance Lake.instTypeNameInputFileDecl :

TypeName InputFileDecl

source

@[implicit_reducible]

instance Lake.instTypeNameInputDirDecl :

TypeName InputDirDecl