[Agda] With and the inspect idiom

[Nils Anders Danielsson]

On Wed, May 14, 2008 at 6:31 PM, Anton Setzer <A.G.Setzer at swansea.ac.uk> wrote:
>
> I tried to follow this thread, but can't follow, since I have never seen
> the construct  with-≡

See Relation.Binary.PropositionalEquality in the standard library:

  http://www.cs.nott.ac.uk/~nad/repos/lib/Relation/Binary/PropositionalEquality.agda

-- 
/NAD