From e2ad18ff1fefa913e884b236b0579df13a2e170c Mon Sep 17 00:00:00 2001 From: rhiannon morris Date: Thu, 16 Nov 2023 18:33:03 +0100 Subject: [PATCH] hello.quox tweaks --- examples/hello.quox | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/examples/hello.quox b/examples/hello.quox index 3b7122e..8e5dbf9 100644 --- a/examples/hello.quox +++ b/examples/hello.quox @@ -12,13 +12,13 @@ def bind : 0.(A B : ★) → IO A → (A → IO B) → IO B = def seq : IO Unit → IO Unit → IO Unit = λ a b ⇒ bind Unit Unit a (λ u ⇒ drop-unit (IO Unit) u b) -#[compile-scheme "(lambda (n) (builtin-io (display n) (newline) 'tt))"] +#[compile-scheme "(lambda (n) (builtin-io (printf \"~d~n\" n) 'tt))"] postulate print-ℕ : ℕ → IO Unit -#[compile-scheme "(lambda (str) (builtin-io (display str) (newline) 'tt))"] +#[compile-scheme "(lambda (s) (builtin-io (printf \"~s~n\" s) 'tt))"] postulate print : String → IO Unit load "nat.quox" #[main] -def main = seq (print-ℕ (nat.plus 1000000000 1)) (print "(nice)") +def main = seq (print-ℕ (nat.plus 60 9)) (print "(nice)")