Data.List.Fresh.Quantifiers

Definitions

data Any : (0 _ : (a -> Type)) -> FreshList a neq -> Type

Totality: total
Visibility: public export
Constructors:

Here : {auto 0 fresh : x # xs} -> p x -> Any p (x :: xs)

There : {auto 0 fresh : x # xs} -> Any p xs -> Any p (x :: xs)

Hint: 

Uninhabited (Any p [])

data All : (0 _ : (a -> Type)) -> FreshList a neq -> Type

Totality: total
Visibility: public export
Constructors:

Nil : All p []

(::) : p x -> {auto 0 fresh : x # xs} -> All p xs -> All p (x :: xs)

lookupWithProof : Any p xs -> (x : a ** p x)

Totality: total
Visibility: public export

lookup : Any p xs -> a

Totality: total
Visibility: public export

remove : Any p xs -> FreshList a neq

Totality: total
Visibility: public export

(!!) : All p xs -> (pos : Any q xs) -> p (lookup pos)

Totality: total
Visibility: public export
Fixity Declaration: infixr operator, level 4

.toFreshList : All p xs -> FreshList (x : a ** p x) (neq `on` .fst)

Totality: total
Visibility: public export

0 .toFreshListFreshness : (rec : All p xs) -> y # xs -> (y ** {_:3734}) # rec .toFreshList

Totality: total
Visibility: public export

traverse : Applicative f => ((x : a) -> p x -> f (q x)) -> All p xs -> f (All q xs)

Totality: total
Visibility: public export

sequence : Applicative f => All (f . p) xs -> f (All p xs)

Totality: total
Visibility: public export

any : ((x : a) -> Dec (p x)) -> (xs : FreshList a neq) -> Dec (Any p xs)

Totality: total
Visibility: public export

isElem : DecEq a => (x : a) -> (xs : FreshList a neq) -> Dec (Any (\{arg:0} => x = {arg:0}) xs)

Totality: total
Visibility: public export

.update : Applicative f => All p xs -> (pos : Any q xs) -> (p (lookup pos) -> f (p (lookup pos))) -> f (All p xs)

Totality: total
Visibility: public export

map : ((x : a) -> p x -> q x) -> Any p xs -> Any q xs

  Map a function

Totality: total
Visibility: public export

map : ((x : a) -> p x -> q x) -> All p xs -> All q xs

  Map a function

Totality: total
Visibility: public export

mapSupport : ((pos : Any f xs) -> q (lookup pos)) -> All f xs -> All q xs

  Map a function restricted to the support of the list

Totality: total
Visibility: public export

tabulate : ((x : a) -> p x) -> All p xs

Totality: total
Visibility: public export

foldl : (b -> a -> b) -> b -> All (const a) xs -> b

Totality: total
Visibility: public export

foldr : (a -> b -> b) -> b -> All (const a) xs -> b

Totality: total
Visibility: public export

insertWith : ((y : a) -> q y -> p y) -> (pos : Any q xs) -> All p (remove pos) -> All p xs

Totality: total
Visibility: public export

insertLookedup : (pos : Any q xs) -> p (lookup pos) -> All p (remove pos) -> All p xs

Totality: total
Visibility: public export