[Agda] Standard library examples?

[Samuel Bronson]

On 5/28/08, Geoffrey Alan Washburn <geoffrey.washburn at epfl.ch> wrote:

> For example, it is not really clear how to do something as simple as
>
>  if (x = y) then ... else ...
>
> where x and y are of type ℕ from Data.Nat and if_then_else_ from Data.Bool.

Actually, Data.Bool isn't involved... You use ℕ-{the equal sign with
the question mark on top} from Data.Nat to do the test, and the magic
"with" to do the branch...

And the reason that the examples in the examples directory of the main
agda repository don't use the standard library is probably related to
the reason Ulf doesn't use it. Examples for the library should
probably be in an examples directory in the library's repository. I've
been getting along fairly well just looking for examples in other
parts of the library ;-).