extern_spec_std_hint_spin_loop

creusot_contracts::std::hint

Function extern_spec_std_hint_spin_loop 

Source 
pub fn extern_spec_std_hint_spin_loop()
Expand description

extern spec for ::std::hint::spin_loop

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

terminates

ghost

requires 

true

ensures 

true