Url in Agda comments

Url.agda

module Url where

-- We usually start something about TT with the definition
-- of ℕ. So here we go:

data ℕ : Set where
  z : ℕ
  s : ℕ → ℕ

-- Now we want to embed a url in the comments. Why not use a
-- simple system of enclosing tokens and a sed script? Like so:
-- [url]https://gist.github.com/gallais/b29706fe7a0ee449b265[/url]

`3 : ℕ
`3 = s (s (s z))

-- We can then produce the html files:
-- agda --html Url.agda
-- And then postprocess them:
-- sed "s/\[url\]\(.*\)\[\/url\]/<a href=\"\1\">\1<\/a>/" html/Url.html > Url.html
-- And get [url]https://rawgit.com/gallais/d167209cd1501f017e5b/raw/Url.html[/url]