Del.agda

module Del where

open import Data.Nat
open import Relation.Binary.Core

data List : Set where
   nil : List
   _::_ : (x : ℕ) -> (xs : List) -> List

-- membership within a list
data _∈_ (x : ℕ) : List -> Set where
   here : forall {xs} -> x ∈ (x :: xs)
   there : forall {xs y} -> (mem : x ∈ xs) -> x ∈ (y :: xs)

-- delete
_\\_ : forall {x} (xs : List) -> (mem : x ∈ xs) -> List
_\\_ nil ()
_\\_ (_ :: xs) here = xs
_\\_ (_ :: nil) (there ())
_\\_ (x :: xs) (there p) = x :: (xs \\ p)

data Foo : List -> Set where
  test : Foo nil
  test2 : forall {x} (xs : List) -> (mem : x ∈ xs) -> Foo (xs \\ mem)

-- Extra proof.
foo : ∀ {xs} → xs ≡ nil → Foo xs → ℕ
foo p  test = 0
foo p  (test2 ys mem) with ys \\ mem
foo p  (test2 _ _) | nil = 1
foo () (test2 _ _) | _ :: _

foo-final : Foo nil → ℕ
foo-final = foo refl