We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
There was an error while loading. Please reload this page.
1 parent f6da121 commit 0039176Copy full SHA for 0039176
theories/Data/String.v
@@ -90,7 +90,7 @@ Section Program_Scope.
90
| true => fun _ => String (digit2ascii n) EmptyString
91
| false => fun pf =>
92
let m := NPeano.div n mod in
93
- append (nat2string m) (String (digit2ascii (n - 10 * m)) EmptyString)
+ append (nat2string m) (String (digit2ascii (n - mod * m)) EmptyString)
94
end eq_refl.
95
Next Obligation.
96
eapply NPeano.Nat.div_lt; auto.
0 commit comments