Module Smyth.Refine

val refine : Lang.hole_ctx -> Lang.datatype_ctx -> Lang.synthesis_goal -> (Lang.exp * Lang.fill_goal list) option

refine delta sigma goal splits the synthesis goal goal into subgoals based on type-and-example-directed refinement.

Type-and-example-directed refinement is deterministic but may fail; hence, this function returns an option.