| Copyright | (c) Nicolás Rodríguez 2021 |
|---|---|
| License | GPL-3 |
| Maintainer | Nicolás Rodríguez |
| Stability | experimental |
| Portability | POSIX |
| Safe Haskell | Safe |
| Language | Haskell2010 |
Data.Tree.BST.Invariants
Description
Type level restrictions for the key ordering in type safe BST trees.
Documentation
type family LtN (l :: Tree) (x :: Nat) :: Bool where ... Source #
Check if all elements of the tree l are strictly less than x.
Equations
| LtN 'EmptyTree _x = 'True | |
| LtN ('ForkTree l (Node n _a) r) x = If (CmpNat n x == 'LT) (If (LtN l x) (If (LtN r x) 'True (TypeError ((('Text "Key " :<>: 'ShowType x) :<>: 'Text " is not strictly lesser than keys in tree ") :<>: 'ShowType r))) (TypeError ((('Text "Key " :<>: 'ShowType x) :<>: 'Text " is not strictly lesser than keys in tree ") :<>: 'ShowType l))) (TypeError ((('Text "Key " :<>: 'ShowType x) :<>: 'Text " is not lesser than key ") :<>: 'ShowType n)) |
type family GtN (r :: Tree) (x :: Nat) :: Bool where ... Source #
Check if all elements of the tree r are strictly greater than x.
Equations
| GtN 'EmptyTree _x = 'True | |
| GtN ('ForkTree l (Node n _a) r) x = If (CmpNat n x == 'GT) (If (GtN l x) (If (GtN r x) 'True (TypeError ((('Text "Key " :<>: 'ShowType x) :<>: 'Text " is not strictly greater than keys in tree ") :<>: 'ShowType r))) (TypeError ((('Text "Key " :<>: 'ShowType x) :<>: 'Text " is not strictly greater than keys in tree ") :<>: 'ShowType l))) (TypeError ((('Text "Key " :<>: 'ShowType x) :<>: 'Text " is not greater than key ") :<>: 'ShowType n)) |