fact: Fixpoint try_all (bs : seq bool) (p : pos) (z : nat) (g : grid) (st : state) (f : grid -> state -> seq grid) {struct bs} : seq grid := if bs is b :: bs1 then if b then let g1 := update p z g in let st1 := update_anti_literals p z st in merge_sudoku (f g1 st1) (try_all bs1 p z.+1 g st f) else try_all bs1 p z.+1 g st f else [::].
imports: mathcomp(all_ssreflect) mathcomp(zify)