[Agda] Standard library examples?

[Samuel Bronson]

On 5/28/08, Peter Berry <pwberry at gmail.com> wrote:
> Maybe another reason is that it's hard to figure out how to type such
> obscure characters. ℕ and some other things I can get with the LaTeX
> input method but as far as I can tell it fails with ≟ (QUESTIONED
> EQUAL TO).

Yeah, I really don't think that was a good idea... I'd be much happier
with \equiv?.