Skip to content

Export to ASCII #211

Open
Open
@stschaef

Description

It's lovely to output actual tikz drawings from the editor, but I was wondering if it would be easy/possible to export to ASCII (or possibly Unicode)

My lab does a lot of category theory proofs in agda, and being able to include well-formatted commutative diagrams as comments is often very helpful. However, these are drawn by hand by us and often look messy. A principled method to generate ASCII diagrams would be used by at least 5 of us (and hopefully other people in the community!)

This is a very low priority issue and I've thought of homebaking something myself but have never found the time. I'd love to hear any thoughts on how you think this could leverage existing code

Thanks

Metadata

Assignees

No one assigned

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions