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:
-- https://gist.github.com/gallais/b29706fe7a0ee449b265

`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 https://rawgit.com/gallais/d167209cd1501f017e5b/raw/Url.html