Data.Tree.BST.Intern.Constructors

Implementation of the constructor of type safe internalist BST trees and instance definition for the Show type class.

Documentation

data BST :: Tree -> Type where

Constructor of internalist BST trees. Given two BST trees and an arbitrary node, it tests at compile time wether the key of the node verifies the LtN and GtN invariants with respect to each tree. Notice that this is all that's needed to assert that the new tree is a BST, since, by recursive logic, both left and right BST trees already respect the key ordering.

Constructors

EmptyBST :: BST 'EmptyTree

ForkBST :: (Show a, LtN l n ~ 'True, GtN r n ~ 'True) => BST l -> Node n a -> BST r -> BST ('ForkTree l (Node n a) r)

Instances

Show (BST t)

Instance definition for the Show type class.

Defined in Data.Tree.BST.Intern.Constructors

Methods

showsPrec :: Int -> BST t -> ShowS

show :: BST t -> String

showList :: [BST t] -> ShowS