Enum KVarEncoding

pub enum KVarEncoding {
    Single,
    Conj,
}

How an rty::KVar is encoded in the fixpoint constraint

Variants

Single

Generate a single kvar appending the self arguments and the scope, i.e., a kvar $k(a0, ...)[b0, ...] becomes $k(a0, ..., b0, ...) in the fixpoint constraint.

Conj

Generate a conjunction of kvars, one per argument in rty::KVar::args. Concretely, a kvar $k(a0, a1, ..., an)[b0, ...] becomes $k0(a0, a1, ..., an, b0, ...) ∧ $k1(a1, ..., an, b0, ...) ∧ ... ∧ $kn(an, b0, ...)

Trait Implementations

impl Clone for KVarEncoding

fn clone(&self) -> KVarEncoding

Returns a copy of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl Copy for KVarEncoding