Data.List.Fresh.Elem

Definitions

data Elem : a -> FreshList a neq -> Type

Totality: total
Visibility: public export
Constructors:

Here : Elem x (x :: xs)

There : Elem y xs -> Elem y (x :: xs)

Hints:

Uninhabited (Here = There e)

Uninhabited (There e = Here)

.recall : (xs : FreshList a neq) -> Elem x xs -> a

Totality: total
Visibility: public export

recallId : (xs : FreshList a neq) -> (pos : Elem x xs) -> xs .recall pos = x

Totality: total
Visibility: public export