Enum RenderIntent 

pub enum RenderIntent {
    Generic,
    Terminal,
    Diff {
        locations: Vec<Address>,
    },
    Signal,
    Delegate,
}

Presentation intent; per-call locations are a pure function of args (tool side). Meta-level declarations use an empty list.

Signal and Delegate carry nothing for the same reason: who a letter goes to and which room takes the work are per call, so a page reads them from the call’s arguments (crates/kernel/spec/Tool.lean D37).

Variants

Generic

Terminal

Diff

Fields

locations: Vec<Address>

Signal

Speaking to another resident, or taking what waits for this one.

Delegate

Handing one piece of work to another room, one level down.

Trait Implementations

impl Clone for RenderIntent

fn clone(&self) -> Self

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for RenderIntent

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

Formats the value using the given formatter.

impl<'de> Deserialize<'de> for RenderIntent

fn deserialize<__D>(__deserializer: __D) -> Result<Self, __D::Error>

where __D: Deserializer<'de>,

Deserialize this value from the given Serde deserializer.

impl Eq for RenderIntent

impl PartialEq for RenderIntent

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

Equality operator ==.

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

Inequality operator !=.

impl Serialize for RenderIntent

fn serialize<__S>(&self, __serializer: __S) -> Result<__S::Ok, __S::Error>

where __S: Serializer,

Serialize this value into the given Serde serializer.

impl StructuralPartialEq for RenderIntent