[Agda] Standard library examples?

[Geoffrey Alan Washburn]

Are there any examples online of using the standard library?  The 
examples included in the examples/ directory do not seem to make use of 
it.  I'm asking because while the library seems to contain many useful 
general abstractions, it is not entirely obvious to me how I should be 
doing many simpler things.

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.  Sure, I know enough to write my own function of type ℕ -> ℕ 
  -> Bool, but I figure it would be good to understand the methodology 
behind the standard library.

If this has come up before, I'm sorry.  I just haven't seen anything on 
the wiki, and gmane's archive of the mailing list only goes back a few 
months.