# doc-gen4

**Repository Path**: zzsj01/doc-gen4

## Basic Information

- **Project Name**: doc-gen4
- **Description**: No description available
- **Primary Language**: Unknown
- **License**: Apache-2.0
- **Default Branch**: LeanInkLink
- **Homepage**: None
- **GVP Project**: No

## Statistics

- **Stars**: 0
- **Forks**: 0
- **Created**: 2023-12-02
- **Last Updated**: 2023-12-03

## Categories & Tags

**Categories**: Uncategorized

**Tags**: None

## README

# doc-gen4
Document Generator for Lean 4

## Usage
`doc-gen4` is the easiest to use via its custom Lake facet, in order
to do this you have to add it to your `lakefile.lean` like this:
```
meta if get_config? env = some "dev" then -- dev is so not everyone has to build it
require «doc-gen4» from git "https://github.com/leanprover/doc-gen4" @ "main"
```
Then you can generate documentation for an entire library using:
```
lake -Kenv=dev build Test:docs
```
If you have multiple libraries you want to generate documentation for
the recommended way right now is to run it for each library.