NOTE: the latest version is 5.0.1

README About Versions Source Modules

BasicTheories.StringTheory

Some basic string proofs

Definition

type NonEmptyString

Basic logic

type alias NonEmptyTrimmedString =

And NonEmptyString TrimmedString

Basic logic

Proofs

mkTrimmedString : String -> Proven String TrimmedString

Basic logic

proveNonEmptyString : String -> Maybe (Proven String NonEmptyString)

Basic logic

proveNonEmptyTrimmedString : String -> Maybe (Proven String NonEmptyTrimmedString)

Basic logic

proveTrimmedString : String -> Maybe (Proven String TrimmedString)

Basic logic

Functions

lengthOfNonEmptyString : Proven String NonEmptyString -> Proven Int Positive

Basic logic

Modules