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