Common/DayPart.lean


1
2
3
4
5
6
7
8
9
10
11
12

namespace DayPart

abbrev Days := {d : Nat // d > 0 ∧ d <= 25}
inductive Parts
| One
| Two

class Parse (day : Days) {ι : outParam Type} where
  parse : String → Except String ι

class Part (day : Days) (part : Parts) {ι ρ : outParam Type} [Parse day (ι := ι)] [ToString ρ] where
  run : ι → Option ρ -- can fail, because it deals with user input...