[Agda] with + continuation

[Peter Divianszky]

Hi,

It would be nice if one could write the following in Agda:

---------------------
module _ (f : (A → B) → C) (g : A → B) where

   c : C
   c withcont f
   ... | a = g a
---------------------

Given 'f : (A → B) → C', 'withcont f' would give a value of 'A' and it 
would replace the goal 'C' with 'B'.

This could be useful in the following situation:

---------------------
open import Data.List using (List; []; _∷_)
open import Data.Empty using (⊥)
open import Relation.Nullary using (Dec; yes; no)
open import Relation.Binary using (Decidable)
open import Relation.Binary.PropositionalEquality using (_≡_; refl)

module Try {A : Set} {{eq : Decidable {A = A} _≡_}} where

   infix 2 _∈_ _∈?_

   data _∈_ (x : A) : List A → Set where
     here : ∀ {xs} → x ∈ x ∷ xs
     there : ∀ {y ys} → x ∈ ys → x ∈ y ∷ ys

   _∈?_ : ∀ (x : A) ys → Dec (x ∈ ys)
   x  ∈? []  = no λ ()
   x  ∈? y ∷ ys with eq x y
   .y ∈? y ∷ ys | yes refl = yes here
   x  ∈? y ∷ ys | no ¬p with x ∈? ys
   x  ∈? y ∷ ys | no ¬p | yes q = yes (there q)
   x  ∈? y ∷ ys | no ¬p | no ¬q = no (f x refl)  where
     f : ∀ a → x ≡ a → (a ∈ y ∷ ys) → ⊥
     f .y e here = ¬p e
     f a e (there r) with a | e
     f a e (there r) | .x | refl = ¬q r
---------------------

This works but I find the following definition of _∈?_ easier to read:

---------------------
   _∈?_ : ∀ (x : A) ys → Dec (x ∈ ys)
   x  ∈? []  = no λ ()
   x  ∈? y ∷ ys with eq x y
   .y ∈? y ∷ ys | yes refl = yes here
   x  ∈? y ∷ ys | no ¬p with x ∈? ys
   x  ∈? y ∷ ys | no ¬p | yes q = yes (there q)
   x  ∈? y ∷ ys | no ¬p | no ¬q withcont no
   .y ∈? y ∷ ys | no ¬p | no ¬q | here    = ¬p e
   x  ∈? y ∷ ys | no ¬p | no ¬q | there r = ¬q r
---------------------

What do you think, is there any chance for 'withcont'?

Cheers,
Peter