1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
|
{-# OPTIONS --guardedness #-}
module Main where
open import Data.Integer.Base as ℤ using (+_)
open import Data.Integer.Literals
open import Data.Integer.GCD
open import Data.Integer.LCM
open import Data.Nat.Base
open import Data.String.Base
open import Data.Unit.Base
open import Function.Base using (_$_)
open import IO.Base
open import IO.Finite
open import Text.Printf
main : Main
main = run $ do
let instance _ = negative
putStrLn $ printf "%s: %u + %u ≡ %u" "example" 3 2 5
putStrLn $ printf "%s: %u + %i ≡ %d" "example" 3 -3 (+ 3 ℤ.+ -3)
putStrLn $ printf "gcd(%d,%i) ≡ %d" -9 (+ 15) (gcd -9 (+ 15))
putStrLn $ printf "lcm(%d,%i) ≡ %d" -9 (+ 15) (lcm -9 (+ 15))
putStrLn $ printf "A %s: %c" "char" 'c'
putStrLn $ printf "A %s: %f" "float" 3.14
|
