From 4a6405ec7a1e5b9cb788735ee41829ceebd56939 Mon Sep 17 00:00:00 2001 From: Jon Eugster Date: Thu, 29 Aug 2024 16:28:13 +0200 Subject: [PATCH] Update README.md --- README.md | 16 ++++++++++++++-- 1 file changed, 14 insertions(+), 2 deletions(-) diff --git a/README.md b/README.md index 5c97abc..d890376 100644 --- a/README.md +++ b/README.md @@ -17,8 +17,20 @@ Once available in your project, you can create import graphs with lake exe graph ``` -A typical command is `lake exe graph --reduce --to MyModule my_graph.pdf` where `MyModule` follows the same module naming you would use to `import` it in lean. -See `lake exe graph --help` for more options. +A typical command is + +``` +lake exe graph --to MyModule my_graph.pdf +``` +where `MyModule` follows the same module naming you would use to `import` it in lean. See `lake exe graph --help` for more options. + +### Json + +To create a Json file, you can use `.xdot_json` as output type: + +``` +lake exe graph my_graph.xdot_json +``` ## Installation