mirror of
https://github.com/polarity-lang/polarity.git
synced 2025-12-23 09:19:50 +00:00
73c9106193
* Add example of set objects * Use boolean methods to clean up codefinitions This also brings the example closer to the paper * Implement interval sets This is implemented in terms of a new `Nat.cmp` operation, along with various predicates on the `Ordering` type (inspired by Rust’s `Ordering` API). * Improve documentation of the set example * Update examples/index.json to include the set.pol * Fix wording of comment
53 lines
839 B
Text
53 lines
839 B
Text
use "./bool.pol"
|
|
|
|
/// The result of comparing two totally-ordered values.
|
|
data Ordering {
|
|
/// Lesser than
|
|
LT,
|
|
/// Equal
|
|
EQ,
|
|
/// Greater than
|
|
GT,
|
|
}
|
|
|
|
/// Returns `T` if the ordering is `EQ`
|
|
def Ordering.isEq: Bool {
|
|
LT => F,
|
|
EQ => T,
|
|
GT => F,
|
|
}
|
|
|
|
/// Returns `T` if the ordering is not `EQ`
|
|
def Ordering.isNe: Bool {
|
|
LT => T,
|
|
EQ => F,
|
|
GT => T,
|
|
}
|
|
|
|
/// Returns `T` if the ordering is `LT`
|
|
def Ordering.isLt: Bool {
|
|
LT => T,
|
|
EQ => F,
|
|
GT => F,
|
|
}
|
|
|
|
/// Returns `T` if the ordering is `GT`
|
|
def Ordering.isGt: Bool {
|
|
LT => F,
|
|
EQ => F,
|
|
GT => T,
|
|
}
|
|
|
|
/// Returns `T` if the ordering is `LT` or `EQ`
|
|
def Ordering.isLe: Bool {
|
|
LT => T,
|
|
EQ => T,
|
|
GT => F,
|
|
}
|
|
|
|
/// Returns `T` if the ordering is `EQ` or `GT`
|
|
def Ordering.isGe: Bool {
|
|
LT => F,
|
|
EQ => T,
|
|
GT => T,
|
|
}
|