rhi/quox
rhi/quox
1
0
Fork 0
Code Issues 15 Pull requests 1 Releases Wiki Activity

hello.quox tweaks

Browse source
This commit is contained in:
rhiannon morris 2023-11-16 18:33:03 +01:00
parent 310822ffa5
commit e2ad18ff1f
1 changed files with 3 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
examples/hello.quox
View file

@ -12,13 +12,13 @@ def bind : 0.(A B : ★) → IO A → (A → IO B) → IO B =
def seq : IO Unit → IO Unit → IO Unit = def seq : IO Unit → IO Unit → IO Unit =
λ a b ⇒ bind Unit Unit a (λ u ⇒ drop-unit (IO Unit) u b) λ 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 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 postulate print : String → IO Unit
load "nat.quox" load "nat.quox"
#[main] #[main]
def main = seq (print-ℕ (nat.plus 1000000000 1)) (print "(nice)") def main = seq (print-ℕ (nat.plus 60 9)) (print "(nice)")