rose-tree

This is a formalization of rose trees in Lean 4.

Usage

To add this library as a dependency, add the following lines to your lakefile.toml and run lake update:

[[require]]
name = "rose-tree"
git = "https://github.com/YellPika/lean-rose-tree"
rev = "main"