link to ascii syntax

rhi 2023-11-04 08:39:52 -04:00
parent 4aa53ca4e7
commit 70e0175575
1 changed files with 2 additions and 0 deletions

@ -1,5 +1,7 @@
\*quox noise*
- if you don't feel like entering all those weird symbols, or you don't have an easy way to do so, an [[ascii syntax]] is also available
## misc notes
- [[agda w-type stuff]]