mtonnberg/refinement-proofs/3.1.0

NOTE: the latest version is 5.0.1

BasicTheories.StringTheory

Some basic string proofs

Definition

A non-empty string

A Trimmed string

A string that are both nonEmpty and trimmed, alias for "And NonEmptyString TrimmedString"

Proofs

Make a trimmed string from a string. Note: will trim a non-trimmed string

proveNonEmptyString : String -> Maybe (Proven String NonEmptyString)

Prove that a string is non-empty

proveNonEmptyTrimmedString : String -> Maybe (Proven String NonEmptyTrimmedString)

Prove that a string is both non-empty and trimmed

proveTrimmedString : String -> Maybe (Proven String TrimmedString)

Prove that a string is trimmed

Functions

Get the length of a non-empty string