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: f24a553de57c3b863f3ace7a23bae81240f65373 (plain) (blame)

namespace Char

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