HepLean Documentation
Lake
.
Toml
.
Load
Search
Google site search
return to top
source
Imports
Init
Lake.Toml.Elab
Lake.Util.Message
Imported by
Lake
.
Toml
.
loadToml
source
def
Lake
.
Toml
.
loadToml
(ictx :
Lean.Parser.InputContext
)
:
EIO
Lean.MessageLog
Lake.Toml.Table
Load a TOML table from some input.
Equations
One or more equations did not get rendered due to their size.
Instances For