README About Versions Source Modules

RefinementProofs.Proofs.ListProofs

Some basic list proofs

Definition

type NonEmptyList

A non-empty list

type SortedList

A sorted list

Proofs

proveNonEmptyList : List a -> Maybe (Proven (List a) NonEmptyList)

Prove that a list is non-empty

mkSortedList : List comparable -> Proven (List comparable) SortedList

Make a sorted list.

Functions

head : Proven (List a) NonEmptyList -> a

Safely get a head of a non-empty list

nonEmptyListMap :

(a -> b)

-> Proven (List a) NonEmptyList

-> Proven (List b) NonEmptyList

Map over a non-empty list

lengthOfNonEmptyList : Proven (List a) NonEmptyList -> Proven Int Positive

Get the length of a non-empty list

Modules