agda-tree

Post-processing agda produced html/*.tree to valid tree.

Install

cargo install agda-tree

Usage

Let's say you have a forest (evergreen notes system via forester), and the directory structure is

.
 |
 |-forest.toml      (config of forester)
 |-trees            (for forester)
 |-xxx
 | |-xxx.agda-lib
 | |- ex.lagda.tree

cd xxx, you first run agda (>= 2.8.0) with flags

agda --html --html-highlight=code ex.lagda.tree

agda will produce a ./html/ex.tree, then do postprocessing

agda-tree build

you will get a directory xxx/trees, I will put this directory into configuration forest.toml, then you can view literate Agda in forster system.

Example