Module Smyth.Branch

val branch : int -> Lang.hole_ctx -> Lang.datatype_ctx -> Lang.hole_filling -> Lang.synthesis_goal -> ((Lang.exp * Lang.fill_goal list) * Lang.constraints) Nondet.t

branch max_scrutinee_size delta sigma hf goal splits the synthesis goal goal into subgoals based on type-and-example-directed branching with a maximum synthesized scrutinee size of max_scrutinee_size.