Few more DafnyStdLibs references

robin-aws · Dec 6, 2023 · d2a7d7d · d2a7d7d
1 parent 66946af
commit d2a7d7d
Show file tree

Hide file tree

Showing 59 changed files with 23 additions and 23 deletions.
diff --git a/Source/DafnyStandardLibraries/CONTRIBUTING.md b/Source/DafnyStandardLibraries/CONTRIBUTING.md
@@ -94,7 +94,7 @@ When `--standard-libraries` is switched on,
 these source files are automatically emitted when compiling,
 just like the contents of each backend's runtime.
 
-See [Makefile](Makefile) and [src/DafnyStdLibs/TargetSpecific/Makefile](src/DafnyStdLibs/TargetSpecific/Makefile) for more details.
+See [Makefile](Makefile) and [src/Std/TargetSpecific/Makefile](src/Std/TargetSpecific/Makefile) for more details.
 
 
 ### On brittleness

diff --git a/Source/DafnyStandardLibraries/Makefile b/Source/DafnyStandardLibraries/Makefile
@@ -15,8 +15,8 @@ verify:
 	$(DAFNY) verify src/dfyconfig-arithmetic.toml
 
 build-binary:
-	$(DAFNY) build -t:lib src/DafnyStdLibs/EnableNonLinearArithmetic/dfyconfig.toml --output:${DOO_FILE_SOURCE}
-	$(DAFNY) build -t:lib src/DafnyStdLibs/DisableNonLinearArithmetic/dfyconfig.toml --output:${DOO_FILE_ARITHMETIC_SOURCE}
+	$(DAFNY) build -t:lib src/Std/EnableNonLinearArithmetic/dfyconfig.toml --output:${DOO_FILE_SOURCE}
+	$(DAFNY) build -t:lib src/Std/DisableNonLinearArithmetic/dfyconfig.toml --output:${DOO_FILE_ARITHMETIC_SOURCE}
 
 check-binary: build-binary
 	unzip -o ${DOO_FILE_SOURCE} -d build/current
@@ -25,12 +25,12 @@ check-binary: build-binary
 	unzip -o ${DOO_FILE_ARITHMETIC_SOURCE} -d build/current-arithmetic
 	unzip -o ${DOO_FILE_ARITHMETIC_TARGET} -d build/rebuilt-arithmetic
 	diff build/current-arithmetic build/rebuilt-arithmetic
-	make -C src/DafnyStdLibs/TargetSpecific check-binary-all
+	make -C src/Std/TargetSpecific check-binary-all
 
 update-binary: build-binary
 	cp ${DOO_FILE_SOURCE} ${DOO_FILE_TARGET}
 	cp ${DOO_FILE_ARITHMETIC_SOURCE} ${DOO_FILE_ARITHMETIC_TARGET}
-	make -C src/DafnyStdLibs/TargetSpecific update-binary-all
+	make -C src/Std/TargetSpecific update-binary-all
 # Rebuild Dafny to pick up the new embedded assets
 	dotnet build ../Dafny.sln
 

diff --git a/Source/DafnyStandardLibraries/README.md b/Source/DafnyStandardLibraries/README.md
@@ -10,7 +10,7 @@ No need to `include` any files! For example:
 ```dafny
 module UsesWrappers {
 
-  import opened DafnyStdLibs.Wrappers
+  import opened Std.Wrappers
 
   function SafeDiv(a: int, b: int): Option<int> {
     if b == 0 then None else Some(a/b)
@@ -45,13 +45,13 @@ In particular, `--standard-libraries` currently cannot be used together with `--
 
 The sections below describe how to use each library:
 
-- [DafnyStdLibs.BoundedInts](src/DafnyStdLibs/BoundedInts) -- definitions of types and constants for fixed-bit-width integers
-- [DafnyStdLibs.Wrappers](src/DafnyStdLibs/Wrappers) -- simple datatypes to support common patterns, such as optional values or the result of operations that can fail
-- [DafnyStdLibs.Relations](src/DafnyStdLibs/Relations) -- properties of relations
-- [DafnyStdLibs.Functions](src/DafnyStdLibs/Functions) -- properties of functions
-- [DafnyStdLibs.Collections](src/DafnyStdLibs/Collections) -- properties of the built-in collection types (seq, set, iset, map, imap, array)
-- DafnyStdLibs.DynamicArray -- an array that can grow and shrink
-- [DafnyStdLibs.Base64](src/DafnyStdLibs/Base64) -- base-64 encoding and decoding
+- [Std.BoundedInts](src/Std/BoundedInts) -- definitions of types and constants for fixed-bit-width integers
+- [Std.Wrappers](src/Std/Wrappers) -- simple datatypes to support common patterns, such as optional values or the result of operations that can fail
+- [Std.Relations](src/Std/Relations) -- properties of relations
+- [Std.Functions](src/Std/Functions) -- properties of functions
+- [Std.Collections](src/Std/Collections) -- properties of the built-in collection types (seq, set, iset, map, imap, array)
+- Std.DynamicArray -- an array that can grow and shrink
+- [Std.Base64](src/Std/Base64) -- base-64 encoding and decoding
 
 We are in the process of importing many more libraries,
 in particular from the existing [`dafny-lang/libraries`](https://github.com/dafny-lang/libraries) GitHub repository.

diff --git a/...NonLinearArithmetic/Arithmetic/DivMod.dfy → ...NonLinearArithmetic/Arithmetic/DivMod.dfy b/...NonLinearArithmetic/Arithmetic/DivMod.dfy → ...NonLinearArithmetic/Arithmetic/DivMod.dfy
diff --git a/...etic/Arithmetic/Internal/DivInternals.dfy → ...etic/Arithmetic/Internal/DivInternals.dfy b/...etic/Arithmetic/Internal/DivInternals.dfy → ...etic/Arithmetic/Internal/DivInternals.dfy
diff --git a/.../Arithmetic/Internal/GeneralInternals.dfy → .../Arithmetic/Internal/GeneralInternals.dfy b/.../Arithmetic/Internal/GeneralInternals.dfy → .../Arithmetic/Internal/GeneralInternals.dfy
diff --git a/...etic/Arithmetic/Internal/ModInternals.dfy → ...etic/Arithmetic/Internal/ModInternals.dfy b/...etic/Arithmetic/Internal/ModInternals.dfy → ...etic/Arithmetic/Internal/ModInternals.dfy
diff --git a/...etic/Arithmetic/Internal/MulInternals.dfy → ...etic/Arithmetic/Internal/MulInternals.dfy b/...etic/Arithmetic/Internal/MulInternals.dfy → ...etic/Arithmetic/Internal/MulInternals.dfy
diff --git a/...Arithmetic/Arithmetic/LittleEndianNat.dfy → ...Arithmetic/Arithmetic/LittleEndianNat.dfy b/...Arithmetic/Arithmetic/LittleEndianNat.dfy → ...Arithmetic/Arithmetic/LittleEndianNat.dfy
diff --git a/...LinearArithmetic/Arithmetic/Logarithm.dfy → ...LinearArithmetic/Arithmetic/Logarithm.dfy b/...LinearArithmetic/Arithmetic/Logarithm.dfy → ...LinearArithmetic/Arithmetic/Logarithm.dfy
diff --git a/...bleNonLinearArithmetic/Arithmetic/Mul.dfy → ...bleNonLinearArithmetic/Arithmetic/Mul.dfy b/...bleNonLinearArithmetic/Arithmetic/Mul.dfy → ...bleNonLinearArithmetic/Arithmetic/Mul.dfy
diff --git a/...eNonLinearArithmetic/Arithmetic/Power.dfy → ...eNonLinearArithmetic/Arithmetic/Power.dfy b/...eNonLinearArithmetic/Arithmetic/Power.dfy → ...eNonLinearArithmetic/Arithmetic/Power.dfy
diff --git a/...NonLinearArithmetic/Arithmetic/Power2.dfy → ...NonLinearArithmetic/Arithmetic/Power2.dfy b/...NonLinearArithmetic/Arithmetic/Power2.dfy → ...NonLinearArithmetic/Arithmetic/Power2.dfy
diff --git a/...bs/DisableNonLinearArithmetic/Strings.dfy → ...td/DisableNonLinearArithmetic/Strings.dfy b/...bs/DisableNonLinearArithmetic/Strings.dfy → ...td/DisableNonLinearArithmetic/Strings.dfy
diff --git a/...ibs/DisableNonLinearArithmetic/Strings.md → ...Std/DisableNonLinearArithmetic/Strings.md b/...ibs/DisableNonLinearArithmetic/Strings.md → ...Std/DisableNonLinearArithmetic/Strings.md
diff --git a/...DisableNonLinearArithmetic/dfyconfig.toml → ...DisableNonLinearArithmetic/dfyconfig.toml b/...DisableNonLinearArithmetic/dfyconfig.toml → ...DisableNonLinearArithmetic/dfyconfig.toml
diff --git a/...metic/Internals/DivInternalsNonlinear.dfy → ...metic/Internals/DivInternalsNonlinear.dfy b/...metic/Internals/DivInternalsNonlinear.dfy → ...metic/Internals/DivInternalsNonlinear.dfy
diff --git a/...metic/Internals/ModInternalsNonlinear.dfy → ...metic/Internals/ModInternalsNonlinear.dfy b/...metic/Internals/ModInternalsNonlinear.dfy → ...metic/Internals/ModInternalsNonlinear.dfy
diff --git a/...metic/Internals/MulInternalsNonlinear.dfy → ...metic/Internals/MulInternalsNonlinear.dfy b/...metic/Internals/MulInternalsNonlinear.dfy → ...metic/Internals/MulInternalsNonlinear.dfy
diff --git a/...eNonLinearArithmetic/Arithmetic/README.md → ...eNonLinearArithmetic/Arithmetic/README.md b/...eNonLinearArithmetic/Arithmetic/README.md → ...eNonLinearArithmetic/Arithmetic/README.md
diff --git a/...Libs/EnableNonLinearArithmetic/Base64.dfy → .../Std/EnableNonLinearArithmetic/Base64.dfy b/...Libs/EnableNonLinearArithmetic/Base64.dfy → .../Std/EnableNonLinearArithmetic/Base64.dfy
diff --git a/...dLibs/EnableNonLinearArithmetic/Base64.md → ...c/Std/EnableNonLinearArithmetic/Base64.md b/...dLibs/EnableNonLinearArithmetic/Base64.md → ...c/Std/EnableNonLinearArithmetic/Base64.md
@@ -1,6 +1,6 @@
 ## The `Base64` module
 
-The `DafnyStdLibs.Base64` module contains an encoder and decoder for Base64, which allows arbitrary byte sequences to be represented in sequences of characters drawn entirely from 7-bit ASCII. This encoder and decoder have two interfaces, one which uses `uint8` to represent arbitrary bytes, and one which uses `bv8`. The encoder and decoder are proved to be inverses of each other, for both interfaces.
+The `Std.Base64` module contains an encoder and decoder for Base64, which allows arbitrary byte sequences to be represented in sequences of characters drawn entirely from 7-bit ASCII. This encoder and decoder have two interfaces, one which uses `uint8` to represent arbitrary bytes, and one which uses `bv8`. The encoder and decoder are proved to be inverses of each other, for both interfaces.
 
 The `uint8`-based interface consists of the `Encode` and `Decode` functions along with the `EncodeDecode` and `DecodeEncode` lemmas. The `bv8`-based interface consists of the `EncodeBV` and `DecodeBV` functions along with the `EncodeDecodeBV` and `DecodeEncodeBV` lemmas. The `uint8`-based interface is a wrapper on top of the `bv8`-based interface, because Base64 encoding is more straightforward to specify and verify using bit vectors.
 

diff --git a/...EnableNonLinearArithmetic/BoundedInts.dfy → ...EnableNonLinearArithmetic/BoundedInts.dfy b/...EnableNonLinearArithmetic/BoundedInts.dfy → ...EnableNonLinearArithmetic/BoundedInts.dfy
diff --git a/.../EnableNonLinearArithmetic/BoundedInts.md → .../EnableNonLinearArithmetic/BoundedInts.md b/.../EnableNonLinearArithmetic/BoundedInts.md → .../EnableNonLinearArithmetic/BoundedInts.md
@@ -1,7 +1,7 @@
 
 ## The `BoundedInts` module
 
-The `DafnyStdLibs.BoundedInts` module contains definitions of types and constants for fixed-bit-width integers.
+The `Std.BoundedInts` module contains definitions of types and constants for fixed-bit-width integers.
 
 Dafny itself generally uses and reasons about mathematical, unbounded integers and natural numbers.
 However compiled programs, for efficiency of computation and storage, will generally use fixed-bit-width
@@ -28,20 +28,20 @@ native signed 8-bit integer type.
 In addition, the module defines a number of constants that are powers of two (not all of them, just those that are generally useful).
 They are useful in stating the ranges of fixed-bit-width integers. Examples are `TWO_TO_THE_15`, `TWO_TO_THE_32`.
 
-Here are two example methods. In the first, the module `DafnyStdLibs.BoundedInts` is renamed to `BI`, which is then used as the prefix for type and constant names.
+Here are two example methods. In the first, the module `Std.BoundedInts` is renamed to `BI`, which is then used as the prefix for type and constant names.
 In the second, the module is imported as opened, in which case the type and constant names can be used without qualification.
 <!-- %check-verify -->
 ```dafny
 module M {
-  import BI = DafnyStdLibs.BoundedInts
+  import BI = Std.BoundedInts
   
   method m(k: BI.int16) {
     assert k as int < BI.TWO_TO_THE_15;
   }
 }
 
 module N {
-  import opened DafnyStdLibs.BoundedInts
+  import opened Std.BoundedInts
 
   method m(k: int16) {
     assert (k/256) as int < TWO_TO_THE_8;

diff --git a/...NonLinearArithmetic/Collections/Array.dfy → ...NonLinearArithmetic/Collections/Array.dfy b/...NonLinearArithmetic/Collections/Array.dfy → ...NonLinearArithmetic/Collections/Array.dfy
diff --git a/...earArithmetic/Collections/Collections.dfy → ...earArithmetic/Collections/Collections.dfy b/...earArithmetic/Collections/Collections.dfy → ...earArithmetic/Collections/Collections.dfy
diff --git a/...nearArithmetic/Collections/Collections.md → ...nearArithmetic/Collections/Collections.md b/...nearArithmetic/Collections/Collections.md → ...nearArithmetic/Collections/Collections.md
diff --git a/...eNonLinearArithmetic/Collections/Imap.dfy → ...eNonLinearArithmetic/Collections/Imap.dfy b/...eNonLinearArithmetic/Collections/Imap.dfy → ...eNonLinearArithmetic/Collections/Imap.dfy
diff --git a/...eNonLinearArithmetic/Collections/Iset.dfy → ...eNonLinearArithmetic/Collections/Iset.dfy b/...eNonLinearArithmetic/Collections/Iset.dfy → ...eNonLinearArithmetic/Collections/Iset.dfy
diff --git a/...leNonLinearArithmetic/Collections/Map.dfy → ...leNonLinearArithmetic/Collections/Map.dfy b/...leNonLinearArithmetic/Collections/Map.dfy → ...leNonLinearArithmetic/Collections/Map.dfy
diff --git a/...leNonLinearArithmetic/Collections/Seq.dfy → ...leNonLinearArithmetic/Collections/Seq.dfy b/...leNonLinearArithmetic/Collections/Seq.dfy → ...leNonLinearArithmetic/Collections/Seq.dfy
diff --git a/...eNonLinearArithmetic/Collections/Sets.dfy → ...eNonLinearArithmetic/Collections/Sets.dfy b/...eNonLinearArithmetic/Collections/Sets.dfy → ...eNonLinearArithmetic/Collections/Sets.dfy
diff --git a/...nableNonLinearArithmetic/DynamicArray.dfy → ...nableNonLinearArithmetic/DynamicArray.dfy b/...nableNonLinearArithmetic/DynamicArray.dfy → ...nableNonLinearArithmetic/DynamicArray.dfy
diff --git a/...s/EnableNonLinearArithmetic/Functions.dfy → ...d/EnableNonLinearArithmetic/Functions.dfy b/...s/EnableNonLinearArithmetic/Functions.dfy → ...d/EnableNonLinearArithmetic/Functions.dfy
diff --git a/...bs/EnableNonLinearArithmetic/Functions.md → ...td/EnableNonLinearArithmetic/Functions.md b/...bs/EnableNonLinearArithmetic/Functions.md → ...td/EnableNonLinearArithmetic/Functions.md
diff --git a/...tdLibs/EnableNonLinearArithmetic/Math.dfy → ...rc/Std/EnableNonLinearArithmetic/Math.dfy b/...tdLibs/EnableNonLinearArithmetic/Math.dfy → ...rc/Std/EnableNonLinearArithmetic/Math.dfy
diff --git a/...StdLibs/EnableNonLinearArithmetic/Math.md → ...src/Std/EnableNonLinearArithmetic/Math.md b/...StdLibs/EnableNonLinearArithmetic/Math.md → ...src/Std/EnableNonLinearArithmetic/Math.md
diff --git a/...s/EnableNonLinearArithmetic/Relations.dfy → ...d/EnableNonLinearArithmetic/Relations.dfy b/...s/EnableNonLinearArithmetic/Relations.dfy → ...d/EnableNonLinearArithmetic/Relations.dfy
diff --git a/...bs/EnableNonLinearArithmetic/Relations.md → ...td/EnableNonLinearArithmetic/Relations.md b/...bs/EnableNonLinearArithmetic/Relations.md → ...td/EnableNonLinearArithmetic/Relations.md
@@ -27,7 +27,7 @@ As a simple example, you might define a predicate like this:
 and then need to prove this lemma to use it in a sorting routine:
 <!-- %check-verify %use tmp-intlt.dfy -->
 ```dafny
-  import opened DafnyStdLibs.Relations
+  import opened Std.Relations
   lemma IntLTisStrictTotalOrder()
     ensures StrictTotalOrdering(IntLT) {}
 ```

diff --git a/...leNonLinearArithmetic/Unicode/Unicode.dfy → ...leNonLinearArithmetic/Unicode/Unicode.dfy b/...leNonLinearArithmetic/Unicode/Unicode.dfy → ...leNonLinearArithmetic/Unicode/Unicode.dfy
diff --git a/...bleNonLinearArithmetic/Unicode/Unicode.md → ...bleNonLinearArithmetic/Unicode/Unicode.md b/...bleNonLinearArithmetic/Unicode/Unicode.md → ...bleNonLinearArithmetic/Unicode/Unicode.md
diff --git a/...nLinearArithmetic/Unicode/UnicodeBase.dfy → ...nLinearArithmetic/Unicode/UnicodeBase.dfy b/...nLinearArithmetic/Unicode/UnicodeBase.dfy → ...nLinearArithmetic/Unicode/UnicodeBase.dfy
diff --git a/...rithmetic/Unicode/UnicodeEncodingForm.dfy → ...rithmetic/Unicode/UnicodeEncodingForm.dfy b/...rithmetic/Unicode/UnicodeEncodingForm.dfy → ...rithmetic/Unicode/UnicodeEncodingForm.dfy
diff --git a/...nearArithmetic/Unicode/UnicodeStrings.dfy → ...nearArithmetic/Unicode/UnicodeStrings.dfy b/...nearArithmetic/Unicode/UnicodeStrings.dfy → ...nearArithmetic/Unicode/UnicodeStrings.dfy
diff --git a/...Unicode/UnicodeStringsWithUnicodeChar.dfy → ...Unicode/UnicodeStringsWithUnicodeChar.dfy b/...Unicode/UnicodeStringsWithUnicodeChar.dfy → ...Unicode/UnicodeStringsWithUnicodeChar.dfy
diff --git a/...rArithmetic/Unicode/Utf16EncodingForm.dfy → ...rArithmetic/Unicode/Utf16EncodingForm.dfy b/...rArithmetic/Unicode/Utf16EncodingForm.dfy → ...rArithmetic/Unicode/Utf16EncodingForm.dfy
diff --git a/...arArithmetic/Unicode/Utf8EncodingForm.dfy → ...arArithmetic/Unicode/Utf8EncodingForm.dfy b/...arArithmetic/Unicode/Utf8EncodingForm.dfy → ...arArithmetic/Unicode/Utf8EncodingForm.dfy
diff --git a/...Arithmetic/Unicode/Utf8EncodingScheme.dfy → ...Arithmetic/Unicode/Utf8EncodingScheme.dfy b/...Arithmetic/Unicode/Utf8EncodingScheme.dfy → ...Arithmetic/Unicode/Utf8EncodingScheme.dfy
diff --git a/...bs/EnableNonLinearArithmetic/Wrappers.dfy → ...td/EnableNonLinearArithmetic/Wrappers.dfy b/...bs/EnableNonLinearArithmetic/Wrappers.dfy → ...td/EnableNonLinearArithmetic/Wrappers.dfy
diff --git a/...ibs/EnableNonLinearArithmetic/Wrappers.md → ...Std/EnableNonLinearArithmetic/Wrappers.md b/...ibs/EnableNonLinearArithmetic/Wrappers.md → ...Std/EnableNonLinearArithmetic/Wrappers.md
@@ -18,7 +18,7 @@ In this library module Dafny defines three such types:
 Consider this routine that looks for a value in a sequence, beginning at position `k`, returning its index:
 <!-- %check-verify %save tmp-find.dfy -->
 ```dafny
-import opened DafnyStdLibs.Wrappers
+import opened Std.Wrappers
 function Find<T(==)>(s: seq<T>, k: int, value: T): (r: Option<int>)
   requires 0 <= k <= |s|
   ensures  r.Some? ==> 0 <= r.Extract() < |s| && s[r.Extract()] == value
@@ -72,7 +72,7 @@ appropriate values in the success situation.
 For example, if we have this method
 <!-- %check-resolve %save tmp-matches.dfy -->
 ```dafny
-import opened DafnyStdLibs.Wrappers
+import opened Std.Wrappers
 method FindAllMatches<T(==)>(s: seq<T>, value: T) returns (status: Outcome<string>, matches: seq<int>)
 ```
 we can call it as
@@ -102,7 +102,7 @@ convert to values of the other types. For example, we can rewrite the example ab
 
 <!-- %check-verify %save tmp-find.dfy -->
 ```dafny
-import opened DafnyStdLibs.Wrappers
+import opened Std.Wrappers
 
 function Find<T(==)>(s: seq<T>, k: int, value: T): (r: Option<int>)
   requires 0 <= k <= |s|
@@ -154,7 +154,7 @@ The workaround, however, is straightforward: just capture the results using `:=`
 
 <!-- %check-verify -->
 ```dafny
-import opened DafnyStdLibs.Wrappers
+import opened Std.Wrappers
 
 method Find<T(==)>(s: seq<T>, k: int, value: T) returns (r: Option<int>, v: T)
   requires 0 <= k <= |s|

diff --git a/.../EnableNonLinearArithmetic/dfyconfig.toml → .../EnableNonLinearArithmetic/dfyconfig.toml b/.../EnableNonLinearArithmetic/dfyconfig.toml → .../EnableNonLinearArithmetic/dfyconfig.toml
diff --git a/...ific/FileIO-notarget-java-cs-js-go-py.dfy → ...ific/FileIO-notarget-java-cs-js-go-py.dfy b/...ific/FileIO-notarget-java-cs-js-go-py.dfy → ...ific/FileIO-notarget-java-cs-js-go-py.dfy
diff --git a/...rgetSpecific/FileIOInternalExterns-go.dfy → ...rgetSpecific/FileIOInternalExterns-go.dfy b/...rgetSpecific/FileIOInternalExterns-go.dfy → ...rgetSpecific/FileIOInternalExterns-go.dfy
diff --git a/...ific/FileIOInternalExterns-java-cs-js.dfy → ...ific/FileIOInternalExterns-java-cs-js.dfy b/...ific/FileIOInternalExterns-java-cs-js.dfy → ...ific/FileIOInternalExterns-java-cs-js.dfy
diff --git a/...ecific/FileIOInternalExterns-notarget.dfy → ...ecific/FileIOInternalExterns-notarget.dfy b/...ecific/FileIOInternalExterns-notarget.dfy → ...ecific/FileIOInternalExterns-notarget.dfy
diff --git a/...rgetSpecific/FileIOInternalExterns-py.dfy → ...rgetSpecific/FileIOInternalExterns-py.dfy b/...rgetSpecific/FileIOInternalExterns-py.dfy → ...rgetSpecific/FileIOInternalExterns-py.dfy
diff --git a/.../src/DafnyStdLibs/TargetSpecific/Makefile → ...Libraries/src/Std/TargetSpecific/Makefile b/.../src/DafnyStdLibs/TargetSpecific/Makefile → ...Libraries/src/Std/TargetSpecific/Makefile
diff --git a/...src/DafnyStdLibs/TargetSpecific/README.md → ...ibraries/src/Std/TargetSpecific/README.md b/...src/DafnyStdLibs/TargetSpecific/README.md → ...ibraries/src/Std/TargetSpecific/README.md
diff --git a/...afnyStdLibs/TargetSpecific/dfyconfig.toml → ...ies/src/Std/TargetSpecific/dfyconfig.toml b/...afnyStdLibs/TargetSpecific/dfyconfig.toml → ...ies/src/Std/TargetSpecific/dfyconfig.toml