This tool is meant to transform Lean files to other documents. Currently what is implemented turns a Lean file with comments into a HTML page. For instance, this webpage was generated from this Lean file.
This tool is meant to transform Lean files to other documents. Currently what is implemented turns a Lean file with comments into a HTML page. For instance, this webpage was generated from this Lean file.