From 81438451fce8b0133d6beeb29b703d334ab3f87a Mon Sep 17 00:00:00 2001 From: "Mark R. Tuttle" Date: Tue, 10 Oct 2023 12:04:19 -0400 Subject: [PATCH] Rename module Math to Dafny.Math The old Math module conflicts with the Java and C# module. This change moved the Math module out of the top-level namespace. --- src/Collections/Sequences/Seq.dfy | 2 +- src/JSON/Serializer.dfy | 2 +- src/Math.dfy | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) diff --git a/src/Collections/Sequences/Seq.dfy b/src/Collections/Sequences/Seq.dfy index d98dcd0b..d8193a07 100644 --- a/src/Collections/Sequences/Seq.dfy +++ b/src/Collections/Sequences/Seq.dfy @@ -23,7 +23,7 @@ module {:options "-functionSyntax:4"} Seq { import opened Wrappers import opened MergeSort import opened Relations - import Math + import Dafny.Math /********************************************************** * diff --git a/src/JSON/Serializer.dfy b/src/JSON/Serializer.dfy index 1f936deb..37c3dee9 100644 --- a/src/JSON/Serializer.dfy +++ b/src/JSON/Serializer.dfy @@ -20,7 +20,7 @@ include "Spec.dfy" module {:options "-functionSyntax:4"} JSON.Serializer { import Seq - import Math + import Dafny.Math import opened Wrappers import opened BoundedInts import opened Utils.Str diff --git a/src/Math.dfy b/src/Math.dfy index 17cf15f2..89890128 100644 --- a/src/Math.dfy +++ b/src/Math.dfy @@ -5,7 +5,7 @@ * SPDX-License-Identifier: MIT *******************************************************************************/ -module {:options "-functionSyntax:4"} Math { +module {:options "-functionSyntax:4"} Dafny.Math { function Min(a: int, b: int): int { if a < b