summaryrefslogtreecommitdiff
path: root/Common/Char.lean
diff options
context:
space:
mode:
Diffstat (limited to 'Common/Char.lean')
-rw-r--r--Common/Char.lean2
1 files changed, 1 insertions, 1 deletions
diff --git a/Common/Char.lean b/Common/Char.lean
index 9c727eb..f24a553 100644
--- a/Common/Char.lean
+++ b/Common/Char.lean
@@ -1,4 +1,4 @@
namespace Char
-def asDigit (d : Char) (ok : Char.isDigit d = true) : Nat :=
+def asDigit (d : Char) (_ : Char.isDigit d = true) : Nat :=
d.toNat - 48