Lines Matching refs:sorry
607 # This makes it easy to replace the proof body with a sorry.
794 '''sorry (* ptr_new_spec_direct *)'''],
798 '''sorry (* ptr_new_spec_path *)'''],
1015 '''sorry (* ptr_empty_union_new_spec_direct *)'''],
1040 '''sorry (* ptr_union_new_spec_direct *)'''],
1155 '''sorry (* ptr_union_set_spec_direct *)'''],
1182 def make_proof(name, substs, sorry=False):
1185 if sorry:
1220 emit_named(fn_name, params, make_proof(prf_prefix + '_direct', substs, params.sorry))
1231 emit_named(fn_name, params, make_proof(prf_prefix + '_path', substs, params.sorry))
1354 substs, params.sorry), file=output)
1358 substs, params.sorry), file=output)
1362 substs, params.sorry), file=output)
1381 params.sorry))
1387 params.sorry))
1390 make_proof('get_tag_spec', substs, params.sorry))
1393 make_proof('get_tag_equals_spec', substs, params.sorry))
1415 params.sorry))
1424 params.sorry))
1432 params.sorry))
1462 params.sorry))
1507 params.sorry))
1517 params.sorry))
1522 make_proof('union_get_spec', substs, params.sorry))
1535 params.sorry))
1545 params.sorry))
1550 make_proof('union_set_spec', substs, params.sorry))
1707 params.sorry)
2315 substs, params.sorry), file=output)
2319 substs, params.sorry), file=output)
2323 substs, params.sorry), file=output)
2341 params.sorry))
2359 params.sorry))
2388 params.sorry))
2397 params.sorry))
2401 make_proof('get_spec', substs, params.sorry))
2412 params.sorry))
2420 params.sorry))
2424 make_proof('set_spec', substs, params.sorry))
2668 dest='sorry', default=False)