[Agda] With and the inspect idiom

[Anton Setzer]

I tried to follow this thread, but can't follow, since I have never seen
the construct  with-≡

Can anybody please explain me what is meant by this code:

foo <something else> with inspect (f b)
 foo <something else> | v with-≡ v≡fb    with f b | v≡fb
 foo <something else> | .(f b) with-≡ ≡-refl | (c , d) | fb≡cd = { }0

(and maybe give a little bit of context, e.g. some example code)?

Thanks,

Anton

-- 
---------------------------------------
Anton Setzer
Department of Computer Science
Swansea University
Singleton Park
Swansea SA2 8PP
UK

Telephone:
(national)        (01792) 513368
(international) +44 1792  513368
Fax:
(national)        (01792) 295708
(international) +44 1792  295708
Visiting address:
Faraday Building,
Computer Science Dept.
2nd floor, room 211.
Email: a.g.setzer at swan.ac.uk
WWW:
http://www.cs.swan.ac.uk/~csetzer/
---------------------------------------