We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
1 parent 79551df commit 8992608Copy full SHA for 8992608
src/JSON/Utils/Str.dfy
@@ -87,12 +87,6 @@ module {:options "-functionSyntax:4"} JSON.Utils.Str {
87
else [minus] + OfNat_any(-n, chars)
88
}
89
90
- function DigitsTable(digits: seq<Char>): map<Char, nat>
91
- requires forall i, j | 0 <= i < j < |digits| :: digits[i] != digits[j]
92
- {
93
- map i: nat | 0 <= i < |digits| :: digits[i] := i
94
- }
95
-
96
function ToNat_any(str: String, base: nat, digits: map<Char, nat>) : (n: nat)
97
requires base > 0
98
requires forall c | c in str :: c in digits
0 commit comments