DecisionTree

Balanced collections let a benchmark keep many refined holes in one value. Each branch records how many leaves belong to its left subtree.
Table of Contents

Types

DecisionTree

(inductive)
Balanced collections let a benchmark keep many refined holes in one value. Each branch records how many leaves belong to its left subtree.
inductive DecisionTree a

Constructors

For each type in this module: inductive types list their declared constructors; opaque types list any local function whose name starts with mk and which returns a value of that type.

DecisionTree (inductive)

leaf

constructor
DecisionTree a

branch

constructor
DecisionTree a

Functions

intAt

Accessors require an index within the collection; generated indices satisfy this by construction. They are monomorphic so their results enter refinements.
def intAt (index : Int) (tree : DecisionTree Int) : Int

boolAt

def boolAt (index : Int) (tree : DecisionTree Bool) : Bool

floatAt

def floatAt (index : Int) (tree : DecisionTree Float) : Float