Module `Smyth.Solve`

val solve_any : Lang.hole_ctx -> Lang.datatype_ctx -> Lang.constraints Nondet.t -> (Lang.hole_filling * Lang.hole_ctx) Nondet.t: solve_any delta sigma possible_ks tries to solve any one of the possible constraints possible_ks. As soon as solve_any finds a solution to one of the possible_ks, it returns that solution (which is a nondeterministic set.)