Enum DestClass 

pub enum DestClass {
    Missing,
    PresentDeclared,
    PresentDirty,
    PresentInProgress,
    PresentUndeclared,
}

Phase 1 per-child destination classifier output.

Lean reference: proof/Grex/Types.lean §“Five-way destination classifier” + theorem classify_dest_total in proof/Grex/Phase1.lean. Every Rust-side classify_dest invocation returns exactly one variant; this is the totality the proof asserts.

Variants

Missing

Path doesn’t exist on disk. Walker will clone here.

PresentDeclared

Path exists, has both .git/ AND a manifest entry, AND the lockfile entry agrees. Walker will fetch (no clone needed).

PresentDirty

Path exists, has .git/ and a manifest entry, lockfile says clean, but the git working tree is dirty (uncommitted changes or untracked files).

PresentInProgress

Path exists with .git/ BUT mid-rebase, mid-merge, mid-cherry-pick, mid-bisect, or mid-revert. Backed by the Lean bridge axiom git_in_progress_decidable. Walker MUST refuse here — both Phase 1 fetch and Phase 2 prune are unsafe.

PresentUndeclared

Path exists, has .git/ BUT no manifest entry declares it. Walker aggregates these into a single TreeError::UntrackedGitRepos error after Phase 1 completes (see aggregate_untracked).

Trait Implementations

impl Clone for DestClass

fn clone(&self) -> DestClass

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for DestClass

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.

impl PartialEq for DestClass

fn eq(&self, other: &DestClass) -> bool

Tests for self and other values to be equal, and is used by ==.

fn ne(&self, other: &Rhs) -> bool

Tests for !=. The default implementation is almost always sufficient, and should not be overridden without very good reason.

impl Copy for DestClass

impl Eq for DestClass

impl StructuralPartialEq for DestClass