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 = (
   ... what does it mean for a list to be sorted ...
);