From 003a63bd13662b750277da75ebd880c97afa23a8 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Fri, 24 Jan 2025 20:21:31 -0800 Subject: [PATCH] doc: Manual about `env.{describe,module_read}` --- doc/repl.md | 2 ++ 1 file changed, 2 insertions(+) diff --git a/doc/repl.md b/doc/repl.md index c7c6f3f..82074e5 100644 --- a/doc/repl.md +++ b/doc/repl.md @@ -13,6 +13,8 @@ See `Pantograph/Protocol.lean` for a description of the parameters and return va only the values of definitions are printed. * `env.save { "path": }`, `env.load { "path": }`: Save/Load the current environment to/from a file +* `env.module_read { "module":