diff --git a/day1-standalone.quox b/day1-standalone.quox index 2b1a733..18c4fa4 100644 --- a/day1-standalone.quox +++ b/day1-standalone.quox @@ -217,8 +217,8 @@ def minus : ℕ → ℕ → ℕ = case dup m return ℕ of { [m] ⇒ elim-pair (λ _ _ ⇒ ℕ) 0 - (λ _ p ⇒ succ p) (λ _ p ⇒ p) + (λ _ p ⇒ succ p) (λ _ _ p ⇒ p) m n } @@ -311,17 +311,13 @@ namespace char { λ x y ⇒ nat.le (ord x) (ord y) def between : ω.Char → ω.Char → ω.Char → Bool = - λ lo hi c ⇒ - case dup c return Bool of { [c] ⇒ bool.and (le lo c) (le c hi) } + λ lo hi c ⇒ bool.and (le lo c) (le c hi) def is-digit : ω.Char → Bool = between (chr 0x30) (chr 0x39) def digit : Char → ℕ = λ c ⇒ nat.minus (ord c) 0x30 - - #[compile-scheme "(lambda (c) (builtin-io (display c) (newline)))"] - postulate println : Char → IO Unit } def0 Char = char.Char