Trait Decidable 

pub trait Decidable {
    type Proof;

    // Required method
    fn decide(&self) -> Decision<Self::Proof>;

    // Provided method
    fn is_decidably_true(&self) -> bool { ... }
}

A type whose truth value is decidable.

Analogous to Lean 4’s Decidable typeclass. Implementors produce a Decision when asked.

Required Associated Types

type Proof

The proof type when the proposition holds.

Required Methods

fn decide(&self) -> Decision<Self::Proof>

Decide the proposition, returning the decision.

Provided Methods

fn is_decidably_true(&self) -> bool

Shorthand: returns true iff the proposition holds.

Implementors

impl<T: PartialEq + Debug> Decidable for EqDecision<T>

type Proof = ()

impl<T: PartialOrd> Decidable for LeDecision<T>

type Proof = ()