Skip to content

Commit

Permalink
Rename module Math->MathLib, name conflicts with Java/C# Math class
Browse files Browse the repository at this point in the history
  • Loading branch information
Mark R. Tuttle committed Oct 4, 2023
1 parent 8b0c399 commit 5dd0601
Show file tree
Hide file tree
Showing 3 changed files with 9 additions and 9 deletions.
8 changes: 4 additions & 4 deletions src/Collections/Sequences/Seq.dfy
Original file line number Diff line number Diff line change
Expand Up @@ -14,7 +14,7 @@
*******************************************************************************/

include "../../Wrappers.dfy"
include "../../Math.dfy"
include "../../MathLib.dfy"
include "MergeSort.dfy"
include "../../Relations.dfy"

Expand All @@ -23,7 +23,7 @@ module {:options "-functionSyntax:4"} Seq {
import opened Wrappers
import opened MergeSort
import opened Relations
import Math
import MathLib

/**********************************************************
*
Expand Down Expand Up @@ -427,7 +427,7 @@ module {:options "-functionSyntax:4"} Seq {
ensures Max(xs) in xs
{
assert xs == [xs[0]] + xs[1..];
if |xs| == 1 then xs[0] else Math.Max(xs[0], Max(xs[1..]))
if |xs| == 1 then xs[0] else MathLib.Max(xs[0], Max(xs[1..]))
}

/* The maximum of the concatenation of two non-empty sequences is greater than or
Expand All @@ -453,7 +453,7 @@ module {:options "-functionSyntax:4"} Seq {
ensures Min(xs) in xs
{
assert xs == [xs[0]] + xs[1..];
if |xs| == 1 then xs[0] else Math.Min(xs[0], Min(xs[1..]))
if |xs| == 1 then xs[0] else MathLib.Min(xs[0], Min(xs[1..]))
}

/* The minimum of the concatenation of two non-empty sequences is
Expand Down
8 changes: 4 additions & 4 deletions src/JSON/Serializer.dfy
Original file line number Diff line number Diff line change
Expand Up @@ -9,7 +9,7 @@

include "../Collections/Sequences/Seq.dfy"
include "../BoundedInts.dfy"
include "../Math.dfy"
include "../MathLib.dfy"

include "Utils/Views.dfy"
include "Utils/Vectors.dfy"
Expand All @@ -20,7 +20,7 @@ include "Spec.dfy"

module {:options "-functionSyntax:4"} JSON.Serializer {
import Seq
import Math
import MathLib
import opened Wrappers
import opened BoundedInts
import opened Utils.Str
Expand Down Expand Up @@ -83,15 +83,15 @@ module {:options "-functionSyntax:4"} JSON.Serializer {

function Number(dec: Values.Decimal): Result<jnumber> {
var minus: jminus := Sign(dec.n);
var num: jnum :- Int(Math.Abs(dec.n));
var num: jnum :- Int(MathLib.Abs(dec.n));
var frac: Maybe<jfrac> := Empty();
var exp: Maybe<jexp> :-
if dec.e10 == 0 then
Success(Empty())
else
var e: je := View.OfBytes(['e' as byte]);
var sign: jsign := Sign(dec.e10);
var num: jnum :- Int(Math.Abs(dec.e10));
var num: jnum :- Int(MathLib.Abs(dec.e10));
Success(NonEmpty(JExp(e, sign, num)));
Success(JNumber(minus, num, Empty, exp))
}
Expand Down
2 changes: 1 addition & 1 deletion src/Math.dfy → src/MathLib.dfy
Original file line number Diff line number Diff line change
Expand Up @@ -5,7 +5,7 @@
* SPDX-License-Identifier: MIT
*******************************************************************************/

module {:options "-functionSyntax:4"} Math {
module {:options "-functionSyntax:4"} MathLib {
function Min(a: int, b: int): int
{
if a < b
Expand Down

0 comments on commit 5dd0601

Please sign in to comment.