Sort

trivial_kernel::table

Trait Sort 

Source 
pub trait Sort {
    // Required methods
    fn is_pure(&self) -> bool;
    fn is_strict(&self) -> bool;
    fn is_provable(&self) -> bool;
    fn is_free(&self) -> bool;
}
Expand description

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§

Source

fn is_pure(&self) -> bool

A pure sort does not allow expression constructors.

Source

fn is_strict(&self) -> bool

A strict sort can not be used as a name.

TODO: explain what a name is.

Source

fn is_provable(&self) -> bool

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

Source

fn is_free(&self) -> bool

A free sort cannot be used as a dummy variable.

Implementors§