[Agda] Converting a pattern match to an equality

[Andreas Abel]

This is an instance of the "inspect" design pattern.

See Relation.Binary.PropositionalEquality in the standard library

------------------------------------------------------------------------
-- The inspect idiom

-- The inspect idiom can be used when you want to pattern match on the
-- result r of some expression e, and you also need to "remember" that
-- r ≡ e.

data Inspect {a} {A : Set a} (x : A) : Set a where
   _with-≡_ : (y : A) (eq : x ≡ y) → Inspect x

inspect : ∀ {a} {A : Set a} (x : A) → Inspect x
inspect x = x with-≡ refl

-- Example usage:

-- f x y with inspect (g x)
-- f x y | c z with-≡ eq = ...


On 2/25/11 5:02 PM, Will Sonnex wrote:
> Is there a way to get the current branch of a pattern match in the
> form of an equality?
>
> For example:
>
> f with t
> ... | k = let h : t ≡ k
>                  h = ?

f with inspect t
... | k with-\equiv h = ...


-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY

andreas.abel at ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/