Skip to content

Commit

Permalink
Avoid stacking newtype definition to avoid bug fixed by dafny #4569
Browse files Browse the repository at this point in the history
  • Loading branch information
robin-aws committed Nov 6, 2023
1 parent 1da5fcd commit dec93a2
Showing 1 changed file with 1 addition and 1 deletion.
Original file line number Diff line number Diff line change
Expand Up @@ -30,7 +30,7 @@ module SearchableEncryptionInfo {
//= specification/searchable-encryption/search-config.md#version-number
//= type=implication
//# A version number MUST be `1`.
newtype VersionNumber = x : uint64 | x == 1 witness 1
newtype VersionNumber = x : int | x == 1 witness 1

type ValidSearchInfo = x : SearchInfo | x.ValidState() witness *

Expand Down

0 comments on commit dec93a2

Please sign in to comment.