[Agda] how do I quote agda code on the agda wiki?

[Ingo Blechschmidt]

Dear Thorsten,

On Thu 21 May 2020 05:47:12 PM GMT, Thorsten Altenkirch wrote:
> I was just adding an item to
> https://wiki.portal.chalmers.se/agda/Main/AIMXXXII
> and tried to add some agda code (I know an unusual thing to do a=on the agda wiki)
[...]

I don't know enough about PmWiki, and therefore will refrain from
updating the "Basic editing" page, but I just fixed the formatting on
the page you linked.

To render code as code, without funny HTML entities ("ℕ" and their
like), you may not use [@...@] but do have to indent the code.

Cheers,
Ingo