Advertisement
Not a member of Pastebin yet?
Sign Up,
it unlocks many cool features!
- {-# LANGUAGE DataKinds #-}
- {-# LANGUAGE GADTs #-}
- data Nat = Z | S Nat
- data Peano n where
- Zero :: Peano Z
- Succ :: Peano n -> Peano (S n)
- type family Leq a b where
- Leq Z b = 'True
- Leq (S a) Z = False
- Leq (S a) (S b) = Leq a b
- type family InRange a b x where
- InRange a b x = Leq a x '&& Leq x b
- tall :: (InRange (S (S Z)) (S (S (S (S Z)))) n ~ 'True) => Peano n
Advertisement
Add Comment
Please, Sign In to add comment
Advertisement