aya-dev icon indicating copy to clipboard operation
aya-dev copied to clipboard

Published 20 hours ago • verified publisher icon aya-prover

Overhaul literate mode

Open ice1000 opened this issue 3 years ago • 1 comments

Now I think mimicking literate Agda is the most sensible way to do everything.

However, things like this are must-do, and can be done by improving org.aya.concrete.remark.CodeAttrProcessor

ice1000 avatar Sep 12 '22 04:09 ice1000

Depends on #464

ice1000 avatar Sep 12 '22 04:09 ice1000