Skip to content

Commit

Permalink
fix: add default value to Opaque constructor (#670)
Browse files Browse the repository at this point in the history
* fix: add default value to Opaque constructor
  • Loading branch information
ajewellamz authored Oct 28, 2024
1 parent 7e5d8c2 commit cff81f5
Show file tree
Hide file tree
Showing 3 changed files with 3 additions and 3 deletions.
Original file line number Diff line number Diff line change
Expand Up @@ -1122,7 +1122,7 @@ module {:extern "software.amazon.cryptography.services.dynamodb.internaldafny.ty


// The Opaque error, used for native, extern, wrapped or unknown errors
| Opaque(obj: object, alt_text : string)
| Opaque(obj: object, alt_text : string := "")
type OpaqueError = e: Error | e.Opaque? witness *
}
abstract module AbstractComAmazonawsDynamodbService {
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -439,7 +439,7 @@ module {:extern "software.amazon.cryptography.services.kms.internaldafny.types"


// The Opaque error, used for native, extern, wrapped or unknown errors
| Opaque(obj: object, alt_text : string)
| Opaque(obj: object, alt_text : string := "")
type OpaqueError = e: Error | e.Opaque? witness *
}
abstract module AbstractComAmazonawsKmsService {
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -1868,7 +1868,7 @@ public TokenTree generateModeledErrorDataType() {
Token.of(
"// The Opaque error, used for native, extern, wrapped or unknown errors"
),
Token.of("| Opaque(obj: object, alt_text : string)"),
Token.of("| Opaque(obj: object, alt_text : string := \"\")"),
// Helper error for use with `extern`
Token.of("type OpaqueError = e: Error | e.Opaque? witness *")
)
Expand Down

0 comments on commit cff81f5

Please sign in to comment.