Trait trivial_kernel::table::Sort[−][src]

pub trait Sort {
    fn is_pure(&self) -> bool;

    fn is_strict(&self) -> bool;

    fn is_provable(&self) -> bool;

    fn is_free(&self) -> bool;
}

A handle to a sort.

Sorts have modifiers that can be queried with this handle. These modifiers correspond to assertions that are verified by the kernel during execution.

Required methods

fn is_pure(&self) -> bool[src]

A pure sort does not allow expression constructors.

fn is_strict(&self) -> bool[src]

A strict sort can not be used as a name.

TODO: explain what a name is.

fn is_provable(&self) -> bool[src]

Only statements with a provable sort can be proven by the kernel.

fn is_free(&self) -> bool[src]

A free sort cannot be used as a dummy variable.

Loading content...

Implementors

impl Sort for Sort_[src]

Loading content...