HepLean Documentation

Lake.Config.ExternLibConfig

structure Lake.ExternLibConfig (pkgName : Lake.Name) (name : Lake.Name) :

A external library's declarative configuration.

Instances For
    Equations
    • Lake.instInhabitedExternLibConfig = { default := { getJob := default } }

    A dependently typed configuration based on its registered package and name.

    Instances For