#[allow(dead_code)]
pub fn to_dafny(
value: &aws_sdk_kms::types::GrantConstraints,
) -> ::dafny_runtime::Rc<
crate::r#software::amazon::cryptography::services::kms::internaldafny::types::GrantConstraints,
> {
::dafny_runtime::Rc::new(
crate::r#software::amazon::cryptography::services::kms::internaldafny::types::GrantConstraints::GrantConstraints {
EncryptionContextSubset:
::dafny_runtime::Rc::new(match &value.encryption_context_subset {
Some(x) => crate::r#_Wrappers_Compile::Option::Some { value :
::dafny_runtime::dafny_runtime_conversions::hashmap_to_dafny_map(x,
|k| dafny_runtime::dafny_runtime_conversions::unicode_chars_false::string_to_dafny_string(&k),
|v| dafny_runtime::dafny_runtime_conversions::unicode_chars_false::string_to_dafny_string(&v),
)
},
None => crate::r#_Wrappers_Compile::Option::None {}
})
,
EncryptionContextEquals:
::dafny_runtime::Rc::new(match &value.encryption_context_equals {
Some(x) => crate::r#_Wrappers_Compile::Option::Some { value :
::dafny_runtime::dafny_runtime_conversions::hashmap_to_dafny_map(x,
|k| dafny_runtime::dafny_runtime_conversions::unicode_chars_false::string_to_dafny_string(&k),
|v| dafny_runtime::dafny_runtime_conversions::unicode_chars_false::string_to_dafny_string(&v),
)
},
None => crate::r#_Wrappers_Compile::Option::None {}
})
,
}
)
}
#[allow(dead_code)]
pub fn from_dafny(
dafny_value: ::dafny_runtime::Rc<
crate::r#software::amazon::cryptography::services::kms::internaldafny::types::GrantConstraints,
>,
) -> aws_sdk_kms::types::GrantConstraints {
aws_sdk_kms::types::GrantConstraints::builder()
.set_encryption_context_subset(match (*dafny_value.EncryptionContextSubset()).as_ref() {
crate::r#_Wrappers_Compile::Option::Some { value } =>
Some(
::dafny_runtime::dafny_runtime_conversions::dafny_map_to_hashmap(value,
|k: &::dafny_runtime::dafny_runtime_conversions::DafnySequence<::dafny_runtime::dafny_runtime_conversions::DafnyCharUTF16>| dafny_runtime::dafny_runtime_conversions::unicode_chars_false::dafny_string_to_string(k),
|v: &::dafny_runtime::dafny_runtime_conversions::DafnySequence<::dafny_runtime::dafny_runtime_conversions::DafnyCharUTF16>| dafny_runtime::dafny_runtime_conversions::unicode_chars_false::dafny_string_to_string(v),
)
),
_ => None
}
)
.set_encryption_context_equals(match (*dafny_value.EncryptionContextEquals()).as_ref() {
crate::r#_Wrappers_Compile::Option::Some { value } =>
Some(
::dafny_runtime::dafny_runtime_conversions::dafny_map_to_hashmap(value,
|k: &::dafny_runtime::dafny_runtime_conversions::DafnySequence<::dafny_runtime::dafny_runtime_conversions::DafnyCharUTF16>| dafny_runtime::dafny_runtime_conversions::unicode_chars_false::dafny_string_to_string(k),
|v: &::dafny_runtime::dafny_runtime_conversions::DafnySequence<::dafny_runtime::dafny_runtime_conversions::DafnyCharUTF16>| dafny_runtime::dafny_runtime_conversions::unicode_chars_false::dafny_string_to_string(v),
)
),
_ => None
}
)
.build()
}