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
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
|
{-# OPTIONS --guardedness #-}
module Main where
open import Data.Bool.Base using (if_then_else_)
open import Data.List.Base using (List; []; _∷_; catMaybes)
open import Data.List.Effectful.Transformer
open import Data.List.Effectful
open import Data.Maybe.Base using (just; nothing)
open import Data.Maybe.Effectful.Transformer
open import Data.Nat.Base using (ℕ; zero; suc; _+_; _^_; _≡ᵇ_)
open import Data.Nat.Show using (show)
open import Data.Product.Base using (_×_; _,_)
open import Data.String.Base using (_++_)
open import Function.Base using (_$_)
open import Effect.Applicative
open import Effect.Monad
open import Effect.Monad.Identity
open import IO.Base using (Main; run)
open import IO.Finite using (putStrLn)
open import Data.List.Instances
open import Data.Maybe.Instances
open import Effect.Monad.Identity.Instances
open import IO.Instances
open RawMonad {{...}}
open RawApplicativeZero {{...}} using (guard)
open TraversableA {{...}}
1⋯100 : List ℕ
1⋯100 = rangeFrom 1 100 where
rangeFrom : (start steps : ℕ) → List ℕ
rangeFrom start zero = []
rangeFrom start (suc n) = start ∷ rangeFrom (suc start) n
triples : MaybeT (ListT Identity) (ℕ × ℕ × ℕ)
triples = do
let range = mkMaybeT (mkListT (pure (pure <$> 1⋯100)))
p ← range
q ← range
r ← range
mkMaybeT (mkListT (pure (pure (guard (p ^ 2 + q ^ 2 ≡ᵇ r ^ 2)))))
pure (p , q , r)
main : Main
main = run
$ ignore $ forA (catMaybes $ runIdentity $ runListT $ runMaybeT triples)
$ λ (p , q , r) → do let sqStr = λ x → show x ++ "²"
putStrLn (sqStr p ++ " + " ++ sqStr q ++ " = " ++ sqStr r)
|
