Languages.RTree

Documentation

data RTree

Constructors

String :>: [RTree]

Instances

Eq RTree

Defined in Languages.RTree

Methods

(==) :: RTree -> RTree -> Bool

(/=) :: RTree -> RTree -> Bool

Show RTree

Defined in Languages.RTree

Methods

showsPrec :: Int -> RTree -> ShowS

show :: RTree -> String

showList :: [RTree] -> ShowS

Arbitrary RTree

Defined in Languages.RTree

Methods

arbitrary :: Gen RTree

shrink :: RTree -> [RTree]

HasDatatypeInfo W FamRTree CodesRTree

Defined in Languages.RTree

Methods

datatypeInfo :: Proxy FamRTree -> SNat ix -> DatatypeInfo (Lkup ix CodesRTree)

Family W FamRTree CodesRTree

Defined in Languages.RTree

Methods

sfrom' :: SNat ix -> El FamRTree ix -> Rep W (El FamRTree) (Lkup ix CodesRTree)

sto' :: SNat ix -> Rep W (El FamRTree) (Lkup ix CodesRTree) -> El FamRTree ix

height :: RTree -> Int

data WKon

Constructors

WString

Instances

TestEquality W

Defined in Languages.RTree

Methods

testEquality :: W a -> W b -> Maybe (a :~: b)

DigestibleHO W

Defined in Languages.RTree

Methods

digestHO :: W ki -> Digest

RendererHO W

Defined in Languages.RTree

Methods

renderHO :: W x -> Doc ann

HasDatatypeInfo W FamRTree CodesRTree

Defined in Languages.RTree

Methods

datatypeInfo :: Proxy FamRTree -> SNat ix -> DatatypeInfo (Lkup ix CodesRTree)

Family W FamRTree CodesRTree

Defined in Languages.RTree

Methods

sfrom' :: SNat ix -> El FamRTree ix -> Rep W (El FamRTree) (Lkup ix CodesRTree)

sto' :: SNat ix -> Rep W (El FamRTree) (Lkup ix CodesRTree) -> El FamRTree ix

data W :: WKon -> * where

Constructors

W_String :: String -> W WString

Instances

TestEquality W

Defined in Languages.RTree

Methods

testEquality :: W a -> W b -> Maybe (a :~: b)

DigestibleHO W

Defined in Languages.RTree

Methods

digestHO :: W ki -> Digest

RendererHO W

Defined in Languages.RTree

Methods

renderHO :: W x -> Doc ann

HasDatatypeInfo W FamRTree CodesRTree

Defined in Languages.RTree

Methods

datatypeInfo :: Proxy FamRTree -> SNat ix -> DatatypeInfo (Lkup ix CodesRTree)

Family W FamRTree CodesRTree

Defined in Languages.RTree

Methods

sfrom' :: SNat ix -> El FamRTree ix -> Rep W (El FamRTree) (Lkup ix CodesRTree)

sto' :: SNat ix -> Rep W (El FamRTree) (Lkup ix CodesRTree) -> El FamRTree ix

Eq (W x)

Defined in Languages.RTree

Methods

(==) :: W x -> W x -> Bool

(/=) :: W x -> W x -> Bool

Show (W x)

Defined in Languages.RTree

Methods

showsPrec :: Int -> W x -> ShowS

show :: W x -> String

showList :: [W x] -> ShowS

type FamRTree = '[RTree, [RTree]]

type CodesRTree = '['['[K WString, I (S Z)]], '['[], '[I Z, I (S Z)]]]

pattern ListRTree_Ifx1 :: phi Z -> phi (S Z) -> View kon phi (Lkup (S Z) CodesRTree)

pattern ListRTree_Ifx0 :: View kon phi (Lkup (S Z) CodesRTree)

pattern RTree_Ifx0 :: kon WString -> phi (S Z) -> View kon phi (Lkup Z CodesRTree)

pattern IdxListRTree :: forall (a :: Nat). () => forall (n :: Nat). (a ~# S n, n ~# Z) => SNat a

pattern IdxRTree :: forall (a :: Nat). () => a ~# Z => SNat a

genConName :: Gen String

genTree :: Int -> Gen RTree

insertAt :: Int -> a -> [a] -> [a]

genInsHere :: RTree -> Gen RTree

genSimilarTrees :: Int -> Gen (RTree, RTree)

genSimilarTreesN :: Int -> Int -> Gen [RTree]

genSimilarTrees' :: Gen (RTree, RTree)

genSimilarTrees'' :: Gen (RTree, RTree, RTree)