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 goalgoal
into subgoals based on type-and-example-directed branching with a maximum synthesized scrutinee size ofmax_scrutinee_size
.