NOTE: the latest version is 5.0.1

README About Versions Source Modules

BasicTheories.NumberTheory

Some basic number proofs

Definition

type Even

Basic logic

type alias Negative =

Not ZeroOrGreater

Basic logic

type alias Odd =

Basic logic

Basic logic

type Zero

Basic logic

type alias ZeroOrGreater =

Or Zero Positive

Basic logic

Proofs

proveEven : Int -> Maybe (Proven Int Even)

Basic logic

proveNegative : number -> Maybe (Proven number Negative)

Basic logic

proveOdd : Int -> Maybe (Proven Int Odd)

Basic logic

provePositive : number -> Maybe (Proven number Positive)

Basic logic

proveZeroOrGreater : number -> Maybe (Proven number ZeroOrGreater)

Basic logic

Implications

allPositivesAreZeroOrGreater : Implies Positive ZeroOrGreater

Basic logic

Modules