<div>{-</div><div><div><br></div><div>Complete Agda module follows:</div><div><br></div><div>The with construct can be a bit tricky at times. There is the inspect idiom that</div><div>you can use, but the problem with that is that you can choose to abstract using</div>

<div>with a normal with, or you can use inspect to get the equation, but you can&#39;t</div><div>have both.</div><div><br></div><div>Enter: Inspect on Steroids.</div></div><div><br></div><div>-}</div><br><div><div>module InspectOnSteroids where</div>

<div><br></div><div>-- Some preliminaries</div><div><br></div><div>data Nat : Set where</div><div>  zero : Nat</div><div>  suc  : Nat → Nat</div><div><br></div><div>data Unit : Set where</div><div>  unit : Unit</div><div>

<br></div><div>data _≡_ {A : Set}(x : A) : A → Set where</div><div>  refl : x ≡ x</div><div><br></div><div>-- The key to steroid-infused inspect is being able to hide terms from the evil with-abstraction monster.</div><div>

<br></div><div>-- The type of hidden terms.</div><div>Hidden : Set → Set</div><div>Hidden A = Unit → A</div><div><br></div><div>-- We can hide a function application</div><div>hide : {A : Set}{B : A → Set} (f : (x : A) → B x) (x : A) → Hidden (B x)</div>

<div>hide f x unit = f x</div><div><br></div><div>-- Revealing a hidden argument is easy.</div><div>reveal : {A : Set} → Hidden A → A</div><div>reveal f = f unit</div><div><br></div><div>-- Inspect on steroids relates hidden values and the corresponding</div>

<div>-- revealed values.</div><div>-- (I&#39;m resisting the temptation to call it reveal_is_).</div><div><br></div><div>data Inspect {A : Set}(x : Hidden A)(y : A) : Set where</div><div>  it : reveal x ≡ y → Inspect x y</div>

<div><br></div><div>-- It&#39;s easy to show that revealing x gives you reveal x:</div><div>inspect : {A : Set}(x : Hidden A) → Inspect x (reveal x)</div><div>inspect f = it refl</div><div><br></div><div>-- Now to use it simply abstract over both the actual term and inspect of the hidden term:</div>

<div><br></div><div>postulate</div><div>  T : Nat → Set</div><div><br></div><div>foo : (f : Nat → Nat)(x : Nat) → T (f x)</div><div>foo f x with f x | inspect (hide f x)</div><div>foo f x | z | it fx=z  = {!!}</div><div>
<br>
</div><div>-- In the hole we have</div><div>-- Goal : T z</div><div>-- fx=z : f x ≡ z</div><div><br></div></div><div>-- / Ulf</div>