[Agda] Converting a pattern match to an equality

[gallais]

Hi will,

You should have a look at inspect in
Relation.Binary.PropositionalEquality (stdlib).

Here is a quick example:

===============================================
open import Data.Nat
open import Relation.Binary.PropositionalEquality

f : ∀ (x y : ℕ) → ℕ
f x y with inspect (suc x)
... | z with-≡ Heq = {!!}
===============================================

Cheers,

--
guillaume

Le Fri, 25 Feb 2011 16:02:57 +0000,
Will Sonnex <will at sonnex.name> a écrit :

> 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 = ?
> 
> 
> Cheers,
> 
> Will
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda