Searched refs:sorry (Results 1 - 5 of 5) sorted by relevance
/seL4-l4v-master/seL4/manual/tools/libsel4_tools/ |
H A D | bitfield_gen.py | 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)) [all...] |
/seL4-l4v-master/seL4/libsel4/tools/ |
H A D | bitfield_gen.py | 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)) [all...] |
/seL4-l4v-master/seL4/tools/ |
H A D | bitfield_gen.py | 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)) [all...] |
/seL4-l4v-master/l4v/misc/pysymbols/isasymbols/ |
H A D | proof.py | 59 def sorry(self): member in class:Proof 62 self.completed = 'sorry'
|
/seL4-l4v-master/l4v/misc/vim/ |
H A D | isabelle.vim | 167 syn keyword IsabelleCommandProofFail sorry oops 653 \ end="\<\(done\|by\|qed\|apply_end\|oops\|sorry\)\>"
|
Completed in 46 milliseconds