Function axiom_cursor_entry_new Copy item path

pub proof fn axiom_cursor_entry_new<'rcu>(
    vm_space: VmSpaceId,
    kind: CursorKind,
    va: Range<Vaddr>,
tracked     owner: CursorOwner<'rcu, UserPtConfig>,
tracked     guards: Guards<'rcu>,
) -> tracked res : CursorEntry<'rcu>

res.vm_space == vm_space,

res.kind == kind,

res.va == va,

res.owner == owner,

res.guards == guards,