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 67 milliseconds