Data.List.Fresh

Fresh lists, a variant of Catarina Coquand's contexts in "A
Formalised Proof of the Soundness and Completeness of a Simply
Typed Lambda-Calculus with Explicit Substitutions"

Based directly on Agda's fresh lists:
http://agda.github.io/agda-stdlib/Data.List.Fresh.html

Reexports

Definitions

BRel : Type -> Type

Totality: total
Visibility: public export

(##) : a -> FreshList a neq -> Bool

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

(#) : a -> FreshList a neq -> Type

Totality: total
Visibility: public export
Fixity Declarations:
infix operator, level 4
infixr operator, level 5

data FreshList : (a : Type) -> BRel a -> Type

Totality: total
Visibility: public export
Constructors:

Nil : FreshList a neq

(::) : (x : a) -> (xs : FreshList a neq) -> {auto 0 _ : x # xs} -> FreshList a neq

data FreshList1 : (a : Type) -> BRel a -> Type

Totality: total
Visibility: public export
Constructor: 

(::) : (x : a) -> (xs : FreshList a neq) -> {auto 0 _ : x # xs} -> FreshList1 a neq

map : {0 A : Type} -> {0 Aneq : BRel A} -> {0 B : Type} -> {0 Bneq : BRel B} -> (F : (A -> B)) -> ((x : A) -> (y : A) -> So (Aneq x y) -> So (Bneq (F x) (F y))) -> FreshList A Aneq -> FreshList B Bneq

Totality: total
Visibility: public export

0 mapFreshness : {0 A : Type} -> {0 Aneq : BRel A} -> {0 B : Type} -> {0 Bneq : BRel B} -> (F : (A -> B)) -> (Injectivity : ((x : A) -> (y : A) -> So (Aneq x y) -> So (Bneq (F x) (F y)))) -> (ys : FreshList A Aneq) -> x # ys -> F x # map ys

Totality: total
Visibility: public export

data Empty : FreshList a neq -> Type

Totality: total
Visibility: public export
Constructor: 

Nil : Empty []

data NonEmpty : FreshList a neq -> Type

Totality: total
Visibility: public export
Constructor: 

IsNonEmpty : NonEmpty (x :: xs)

length : FreshList a neq -> Nat

Totality: total
Visibility: public export

fromMaybe : Maybe a -> FreshList a neq

Totality: total
Visibility: public export

uncons : FreshList a neq -> Maybe (a, FreshList a neq)

Totality: total
Visibility: public export

toFreshList1 : FreshList a neq -> Maybe (FreshList1 a neq)

Totality: total
Visibility: public export

head : (xs : FreshList a neq) -> NonEmpty xs => a

Totality: total
Visibility: public export

tail : (xs : FreshList a neq) -> NonEmpty xs => FreshList a neq

Totality: total
Visibility: public export

0 .freshness : (xs : FreshList a neq) -> {auto isNonEmpty : NonEmpty xs} -> head xs # tail xs

Totality: total
Visibility: public export

0 headFreshness : (0 x : a) -> (ys : FreshList a neq) -> {auto isNonEmpty : NonEmpty ys} -> x # ys -> So (neq x (head ys))

Totality: total
Visibility: public export

0 tailFreshness : (0 x : a) -> (ys : FreshList a neq) -> {auto isNonEmpty : NonEmpty ys} -> x # ys -> x # tail ys

Totality: total
Visibility: public export

take : Nat -> FreshList a neq -> FreshList a neq

Totality: total
Visibility: public export

0 takeFreshness : (n : Nat) -> (xs : FreshList a neq) -> y # xs -> y # take n xs

Totality: total
Visibility: public export

drop : Nat -> FreshList a neq -> FreshList a neq

Totality: total
Visibility: public export

takeWhile : (a -> Bool) -> FreshList a neq -> FreshList a neq

Totality: total
Visibility: public export

0 takeWhileFreshness : (pred : (a -> Bool)) -> (xs : FreshList a neq) -> y # xs -> y # takeWhile pred xs

Totality: total
Visibility: public export

dropWhile : (a -> Bool) -> FreshList a neq -> FreshList a neq

Totality: total
Visibility: public export

0 dropWhileFreshness : (pred : (a -> Bool)) -> (xs : FreshList a neq) -> y # xs -> y # dropWhile pred xs

Totality: total
Visibility: public export

filter : (a -> Bool) -> FreshList a neq -> FreshList a neq

Totality: total
Visibility: public export

0 filterFreshness : (pred : (a -> Bool)) -> (xs : FreshList a neq) -> y # xs -> y # filter pred xs

Totality: total
Visibility: public export

decideFreshness : (x : a) -> (ys : FreshList a neq) -> Dec (x # ys)

Totality: total
Visibility: public export

foldl : (b -> a -> b) -> b -> FreshList a neq -> b

Totality: total
Visibility: public export

foldr : (a -> b -> b) -> b -> FreshList a neq -> b

Totality: total
Visibility: public export

(##) : BRel String

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

FreshSnoc : SnocList a -> FreshList a neq -> Type

Totality: total
Visibility: public export

castAux : (sx : SnocList a) -> (xs : FreshList a neq) -> {auto 0 _ : FreshSnoc sx xs} -> FreshList a neq

Totality: total
Visibility: public export

Fresh : SnocList a -> Type

Totality: total
Visibility: public export

cast : (sx : SnocList a) -> {auto 0 _ : Fresh sx} -> FreshList a neq

Totality: total
Visibility: public export