Function extern_spec_core_intrinsics_discriminant_value 

pub fn extern_spec_core_intrinsics_discriminant_value<T>(
    v: &T,
) -> <T as DiscriminantKind>::Discriminant

extern spec for ::core::intrinsics::discriminant_value<T>

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

ghost

ensures

#[logic_alias(discriminant_value_logic(*v))]