Generics.MRSOP.Examples.RoseTree

Contents

• Standard Rose-Tree datatype
  • Family Structure
  • Instance Decl
• Eq Instance
• Compos test
• Crush test
• Orphan instances

Description

Synopsis

• data R a
  • = a :>: [R a]
  • | Leaf a
• value1 :: R Int
• value2 :: R Int
• value3 :: R Int
• type ListCode = '['[], '[I (S Z), I Z]]
• type RTCode = '['[K KInt, I Z], '[K KInt]]
• type CodesRose = '[ListCode, RTCode]
• type FamRose = '[[R Int], R Int]
• testEq :: Bool
• pattern RInt_ :: forall (a :: Nat). () => forall (n :: Nat). ((~#) Nat Nat a (S n), (~#) Nat Nat n Z) => SNat a
• normalize :: R Int -> R Int
• sumTree :: R Int -> Int
• testSum :: Bool

Standard Rose-Tree datatype

Family Structure

Instance Decl

Eq Instance

Compos test

Crush test

Orphan instances