aws_db_esdk/deps/aws_cryptography_dbEncryptionSdk_dynamoDb/conversions/
constructor.rs1#[allow(dead_code)]
5pub fn to_dafny(
6 value: &crate::deps::aws_cryptography_dbEncryptionSdk_dynamoDb::types::Constructor,
7) -> ::dafny_runtime::Rc<
8 crate::r#software::amazon::cryptography::dbencryptionsdk::dynamodb::internaldafny::types::Constructor,
9>{
10 ::dafny_runtime::Rc::new(to_dafny_plain(value.clone()))
11}
12
13#[allow(dead_code)]
14pub fn to_dafny_plain(
15 value: crate::deps::aws_cryptography_dbEncryptionSdk_dynamoDb::types::Constructor,
16) -> crate::r#software::amazon::cryptography::dbencryptionsdk::dynamodb::internaldafny::types::Constructor{
17 crate::r#software::amazon::cryptography::dbencryptionsdk::dynamodb::internaldafny::types::Constructor::Constructor {
18 parts: ::dafny_runtime::dafny_runtime_conversions::vec_to_dafny_sequence(&value.parts.clone().unwrap(),
19 |e| crate::deps::aws_cryptography_dbEncryptionSdk_dynamoDb::conversions::constructor_part::to_dafny(&e.clone())
20,
21)
22,
23 }
24}
25
26#[allow(dead_code)]
27pub fn option_to_dafny(
28 value: ::std::option::Option<crate::deps::aws_cryptography_dbEncryptionSdk_dynamoDb::types::Constructor>,
29) -> ::dafny_runtime::Rc<crate::_Wrappers_Compile::Option<::dafny_runtime::Rc<
30 crate::r#software::amazon::cryptography::dbencryptionsdk::dynamodb::internaldafny::types::Constructor,
31>>>{
32 ::dafny_runtime::Rc::new(match value {
33 ::std::option::Option::None => crate::_Wrappers_Compile::Option::None {},
34 ::std::option::Option::Some(x) => crate::_Wrappers_Compile::Option::Some {
35 value: ::dafny_runtime::Rc::new(to_dafny_plain(x)),
36 },
37 })
38}
39
40#[allow(dead_code)]
41pub fn from_dafny(
42 dafny_value: ::dafny_runtime::Rc<
43 crate::r#software::amazon::cryptography::dbencryptionsdk::dynamodb::internaldafny::types::Constructor,
44 >,
45) -> crate::deps::aws_cryptography_dbEncryptionSdk_dynamoDb::types::Constructor {
46 plain_from_dafny(&*dafny_value)
47}
48
49#[allow(dead_code)]
50pub fn plain_from_dafny(
51 dafny_value: &crate::r#software::amazon::cryptography::dbencryptionsdk::dynamodb::internaldafny::types::Constructor,
52) -> crate::deps::aws_cryptography_dbEncryptionSdk_dynamoDb::types::Constructor {
53 match dafny_value {
54 crate::r#software::amazon::cryptography::dbencryptionsdk::dynamodb::internaldafny::types::Constructor::Constructor {..} =>
55 crate::deps::aws_cryptography_dbEncryptionSdk_dynamoDb::types::Constructor::builder()
56 .set_parts(Some( ::dafny_runtime::dafny_runtime_conversions::dafny_sequence_to_vec(dafny_value.parts(),
57 |e: &::dafny_runtime::Rc<crate::r#software::amazon::cryptography::dbencryptionsdk::dynamodb::internaldafny::types::ConstructorPart>| crate::deps::aws_cryptography_dbEncryptionSdk_dynamoDb::conversions::constructor_part::from_dafny(e.clone())
58,
59)
60 ))
61 .build()
62 .unwrap()
63 }
64}
65
66#[allow(dead_code)]
67pub fn option_from_dafny(
68 dafny_value: ::dafny_runtime::Rc<crate::_Wrappers_Compile::Option<::dafny_runtime::Rc<
69 crate::r#software::amazon::cryptography::dbencryptionsdk::dynamodb::internaldafny::types::Constructor,
70 >>>,
71) -> ::std::option::Option<crate::deps::aws_cryptography_dbEncryptionSdk_dynamoDb::types::Constructor>
72{
73 match &*dafny_value {
74 crate::_Wrappers_Compile::Option::Some { value } => {
75 ::std::option::Option::Some(plain_from_dafny(value))
76 }
77 _ => ::std::option::Option::None,
78 }
79}