Lines Matching defs:check
11 import check
12 from check import restr_others, loops_to_split, ProofNode
57 init_hyps = check.init_point_hyps (p)
87 def check (i):
106 map (check, check_order)
109 check (split)
742 hyps = check.init_point_hyps (p)
828 (r_start, r_step), 'Seq check failed'))
870 hyps = hyps + [check.non_r_err_pc_hyp (tags,
1187 hyp = check.single_induct_resulting_hyp (p, restrs, spec)
1256 checks = check.split_init_step_checks (rep.p, restrs,
1332 (verdict, _) = check.test_hyp_group (rep, checks2)
1409 hyps = hyps + check.split_loop_hyps (tags, split, restrs, exit = True)
1486 checks = (check.single_loop_rev_induct_checks (p, restrs, hyps, tag,
1488 + check.single_loop_rev_induct_base_checks (p, restrs, hyps,
1491 groups = check.proof_check_groups (checks)
1493 (res, _) = check.test_hyp_group (rep, group)
1600 """perform both the induction check and a function-call based check
1606 err_hyp = check.split_r_err_pc_hyp (p, split, restrs, tags = tags)
1607 hyps = [err_hyp] + hyps + check.split_loop_hyps (tags, split,
1612 if not check.check_split_induct_step_group (rep, restrs, hyps, split,
1679 hyp = check.single_induct_resulting_hyp (rep.p, restrs, spec)
1720 probs = check.proof_subproblems (p, kind, details, restrs, hyps, name)
1730 restr_points = check.split_heads (details)
1752 nrerr_hyp = check.non_r_err_pc_hyp (p.pairing.tags,
1785 # double-check this limit with a rep constructed without the 'fast' flag
1855 xs = set ([p.loop_id (h) for h in check.split_heads (split)])