Juvix Markdown Structure¶

File Structure¶

A Juvix Markdown file (.juvix.md) must follow these rules:

• The first Juvix code block must declare a module matching the file name
• Code blocks must contain well-defined Juvix expressions
• Module names must follow folder structure

Example:

module tutorial.basics;
-- ...

Code Block Features¶

Enable Juvix code blocks in mkdocs.yml:

plugins:
  - juvix

Hiding Code Blocks¶

Hide code blocks using the hide attribute:

````juvix hide
module tutorial.basics;
-- ...
```

Extracting Module Statements¶

Extract inner module statements:

````juvix extract-module-statements
module B;
module C;
-- ...
```

With a specific number of statements:

````juvix extract-module-statements 2
module B;
axiom a : Nat;
module C;
-- ...
```

Disabling Processing¶

Disable Juvix processing per file:

---
preprocess:
  juvix: false
---