NOTE: the latest version is 5.0.1

README About Versions Source Modules

BasicTheories.ListTheory

Some basic list proofs

Definition

type NonEmptyList

Basic logic

type SortedList

Basic logic

Proofs

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

Basic logic

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

Basic logic

Functions

head : Proven (List a) NonEmptyList -> a

Basic logic

nonEmptyListMap :

(a -> b)

-> Proven (List a) NonEmptyList

-> Proven (List b) NonEmptyList

Basic logic

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

Basic logic

Modules