Struct Node

struct Node {
    kind: NodeKind,
    nbindings: usize,
    parent: Option<WeakNodePtr>,
    children: Vec<NodePtr>,
}

Fields

kind: NodeKind

nbindings: usize

Number of bindings between the root and this node’s parent, i.e., we have as an invariant that nbindings equals the number of NodeKind::ForAll nodes from the parent of this node to the root.

parent: Option<WeakNodePtr>

children: Vec<NodePtr>

Implementations

impl Node

fn simplify(&mut self, genv: GlobalEnv<'_, '_>)

fn is_leaf(&self) -> bool

fn replace_evars(&mut self, evars: &EVarStore) -> Result<(), EVid>

fn to_fixpoint( &self, cx: &mut FixpointCtxt<'_, '_, Tag>, ) -> QueryResult<Option<Constraint>>

fn is_forall(&self) -> bool

Returns true if the node kind is ForAll.

fn is_head(&self) -> bool

Returns true if the node kind is Head.