Char.lean « Common - aoc-2023 - Advent of Code 2023 - I'm still learning Lean4, so please don't judge.

summary refs log tree commit diff

path: root/Common/Char.lean

blob: 9c727eb54a5f9bd367769f07612db59e8cef1ad7 (plain) (blame)

namespace Char

def asDigit (d : Char) (ok : Char.isDigit d = true) : Nat :=
  d.toNat - 48