Structures.Dependent.FreshList

Reexports

Definitions

(##) : e -> FreshList fresh e -> Bool

  Checks if a new element is 'fresh' against all the existing elements of the
  given `FreshList`
  @ e is the type of the elments in the list
  @ x is the new element being checked for freshness
  @ xs is the existing `FreshList`
  @ fresh is the freshness criteria

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

(#) : e -> FreshList fresh e -> Type

  Wrapper for `##` that lifts the check up to the type level using `So`

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

data FreshList : (e -> e -> Bool) -> Type -> Type

Totality: total
Visibility: public export
Constructors:

Nil : FreshList fresh e

(::) : (x : e) -> (xs : FreshList fresh e) -> {auto 0 _ : x # xs} -> FreshList fresh e

Hints:

Eq e => Eq (FreshList fresh e)

Foldable (FreshList fresh)

Ord e => Ord (FreshList fresh e)

Show e => Show (FreshList fresh e)

fromList : List e -> Maybe (FreshList fresh e)

  Attempt to convert a regular `List` to a `FreshList`
  
  This will validate the freshness criteria as it goes along, returning `Just`
  if all elements are fresh, and `Nothing` if any elements are non-fresh
  
  @ fresh is the freshness criteria
  @ e is the type of the elements in the list
  @ xs is the list to convert

Visibility: public export

data NonEmpty : FreshList fresh e -> Type

  Witness that a FreshList is non-empty

Totality: total
Visibility: public export
Constructor: 

IsNonEmpty : NonEmpty (x :: xs)

data Empty : FreshList fresh e -> Type

  Witness that a FreshList is empty

Totality: total
Visibility: public export
Constructor: 

IsEmpty : Empty []

length : FreshList fresh e -> Nat

  Return the number of elements in the provided `FreshList`

Visibility: export

find : (e -> Bool) -> FreshList fresh e -> Maybe e

  Return the first element of this `FreshList` satisfying the given predicate,
  if there is one

Visibility: export