doc: Manual about `env.{describe,module_read}`

This commit is contained in:
Leni Aniva 2025-01-24 20:21:31 -08:00
parent b67d3eccc4
commit 003a63bd13
Signed by: aniva
GPG Key ID: 4D9B1C8D10EA4C50
1 changed files with 2 additions and 0 deletions

View File

@ -13,6 +13,8 @@ See `Pantograph/Protocol.lean` for a description of the parameters and return va
only the values of definitions are printed. only the values of definitions are printed.
* `env.save { "path": <fileName> }`, `env.load { "path": <fileName> }`: Save/Load the * `env.save { "path": <fileName> }`, `env.load { "path": <fileName> }`: Save/Load the
current environment to/from a file current environment to/from a file
* `env.module_read { "module": <name }`: Reads a list of symbols from a module
* `env.describe {}`: Describes the imports and modules in the current environment
* `options.set { key: value, ... }`: Set one or more options (not Lean options; those * `options.set { key: value, ... }`: Set one or more options (not Lean options; those
have to be set via command line arguments.), for options, see `Pantograph/Protocol.lean` have to be set via command line arguments.), for options, see `Pantograph/Protocol.lean`