Skip to content

Commit

Permalink
Update README.md
Browse files Browse the repository at this point in the history
  • Loading branch information
joneugster authored Aug 29, 2024
1 parent 57bd206 commit 4a6405e
Showing 1 changed file with 14 additions and 2 deletions.
16 changes: 14 additions & 2 deletions README.md
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand Down

0 comments on commit 4a6405e

Please sign in to comment.