Dear Agda list, Is there any documentation which explains how the Agda "with" pattern-matchign notation is used? It's mentioned on the wiki, but only with "..." on the left-hand side of the bar. many thanks, Roly