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 goalgoal
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
.