Function extern_spec_T_A_Rc_T_A_as_ptr 

pub fn extern_spec_T_A_Rc_T_A_as_ptr<T, A: Allocator>(
    this: &Rc<T, A>,
) -> *const T

extern spec for Rc<T, A>::as_ptr

This is not a real function: its only use is for documentation.

terminates

ghost

ensures

result == this.as_ptr_logic()

ensures

!result.is_null_logic()