pub(crate) fn invariants_of(
genv: GlobalEnv<'_, '_>,
def_id: MaybeExternId,
) -> EarlyBinder<List<Invariant>>Expand description
Errors are reported at the definition of the adt. If the invariants fail to convert, we continue as if the adt had no invariants. This is sound because the invariants are then neither checked (when constructing the adt) nor assumed (when using it).