Propositional Types

A propositional type is a type that is not a traditional datatype but rather asserts some other logical "property" on a term.

Declaring a Propositional Type

Declaring a Corollary

A corollary is a function that produces only propositional types as a return value. Corollaries are used to enrich existing terms with new type information.

let prop assert-is-sorted(x: List<i>): List::Sorted = (
   ... prove that the list is sorted ...
);

Auto Proof Tactics

Rather than drafting statements directly, LSTS @auto(goal) tries to connect a term to a goal using only corollaries. If this is found to be difficult or impossible then auto-proof will just give up.