blob: 4098b3c6679b7897ddf50e04d20ef8be1285a4f5 (
plain)
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
|
{-# LANGUAGE DataKinds, TypeOperators, TypeFamilies #-}
module Main(main) where
import GHC.TypeLits
import Data.Proxy
--------------------------------------------------------------------------------
-- Test top-reactions
tsub :: Proxy (x + y) -> Proxy y -> Proxy x
tsub _ _ = Proxy
tdiv :: Proxy (x * y) -> Proxy y -> Proxy x
tdiv _ _ = Proxy
troot :: Proxy (x ^ y) -> Proxy y -> Proxy x
troot _ _ = Proxy
tlog :: Proxy (x ^ y) -> Proxy x -> Proxy y
tlog _ _ = Proxy
tleq :: ((x <=? y) ~ True) => Proxy y -> Proxy x
tleq _ = Proxy
main :: IO ()
main = print [ sh (tsub (Proxy :: Proxy 5) (Proxy :: Proxy 3)) == "2"
, sh (tdiv (Proxy :: Proxy 8) (Proxy :: Proxy 2)) == "4"
, sh (troot (Proxy :: Proxy 9) (Proxy :: Proxy 2)) == "3"
, sh (tlog (Proxy :: Proxy 8) (Proxy :: Proxy 2)) == "3"
, sh (tleq (Proxy :: Proxy 0)) == "0"
]
where
sh x = show (natVal x)
|
