RefinementProofs.Proofs.NumberProofs

Some basic number proofs

Definition

type Even

An even Int

type alias Negative =

Not ZeroOrGreater

A negative number. Alias for Not ZeroOrGreater

type alias Odd =

Not Even

alias for Not Even

type Positive

A positive number

type Zero

A number that is Zero

type alias ZeroOrGreater =

Or Zero Positive

type alias for Or Zero Positive. If used with an Int this the number is 0,1,2,3,....

Proofs

proveEven : Int -> Maybe (Proven Int Even)

Prove that a number is even

proveNegative : number -> Maybe (Proven number Negative)

Prove a number is negative

proveOdd : Int -> Maybe (Proven Int Odd)

Prove that a number is odd

provePositive : number -> Maybe (Proven number Positive)

Prove that a number is positive (>0)

proveZeroOrGreater : number -> Maybe (Proven number ZeroOrGreater)

Prove that a number is either zero or greater

Implications

allPositivesAreZeroOrGreater : Implies Positive ZeroOrGreater

A simple implication. Note this is strictly not needed since this implication is clear in the types - ZeroOrGreater = Or Zero Positive. An alternative is to use introOrL or or.

mtonnberg/refinement-proofs/5.0.1

RefinementProofs.Proofs.NumberProofs

Definition

Proofs

Implications

Modules