From 16be5d673739c61aeb81e1e38aba0890426ef42a Mon Sep 17 00:00:00 2001 From: Robin Salkeld Date: Fri, 13 Oct 2023 16:21:01 -0700 Subject: [PATCH] Rename, work around Go bug --- .../src/{dafny => dafnystdlibs}/Wrappers.dfy | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) rename Source/DafnyStandardLibraries/src/{dafny => dafnystdlibs}/Wrappers.dfy (98%) diff --git a/Source/DafnyStandardLibraries/src/dafny/Wrappers.dfy b/Source/DafnyStandardLibraries/src/dafnystdlibs/Wrappers.dfy similarity index 98% rename from Source/DafnyStandardLibraries/src/dafny/Wrappers.dfy rename to Source/DafnyStandardLibraries/src/dafnystdlibs/Wrappers.dfy index d8735b64994..f2c57ff6f04 100644 --- a/Source/DafnyStandardLibraries/src/dafny/Wrappers.dfy +++ b/Source/DafnyStandardLibraries/src/dafnystdlibs/Wrappers.dfy @@ -210,7 +210,7 @@ module {:options "--function-syntax:4"} DafnyStdLibs.Wrappers { /** In verification, this method functions as an `assert` of the given condition; at run-time functions as an `expect`. The arguments may not be ghost. */ - method AssertAndExpect(condition: bool, maybeMsg: Option := None) + method AssertAndExpect(condition: bool, maybeMsg: Option := None) requires condition { match maybeMsg {