git.iko.soy/Idris-dev
on master help sign in
Idris-dev/samples/effects/Select.idr
17 lines 488 B history raw
1module Main
3import Effects
4import Effect.Select
5import Effect.Exception
7triple : Int -> { [SELECT, EXCEPTION String] } Eff (Int, Int, Int)
8triple max = do z <- select [1..max]
9 y <- select [1..z]
10 x <- select [1..y]
11 if (x * x + y * y == z * z)
12 then pure (x, y, z)
13 else raise "No triple"
15main : IO ()
16main = do print $ the (Maybe _) $ run (triple 100)
17 print $ the (List _) $ run (triple 100)