Searched defs:pv (Results 1 - 9 of 9) sorted by path

/seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/cheri/step/
H A Dcheri_stepLib.sml239 val pv = padded_opcode v value
/seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/common/
H A Dcore_decompilerLib.sml49 let val pv = add_prime v in [v |-> pv, pv |-> v] end) vs)) value
H A DutilsLib.sml1252 fun pv q = Q.prove (q, tac) function
/seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/mips/step/
H A Dmips_stepLib.sml991 val pv = padded_opcode v value
/seL4-l4v-10.1.1/HOL4/examples/machine-code/graph/
H A Dderive_specsLib.sml88 val pv = free_vars p |> filter (fn tm => type_of tm = ``:bool``) value
/seL4-l4v-10.1.1/HOL4/examples/separationLogic/src/holfoot/
H A Dholfoot_pp_print.sml1050 val (pv, spec) = pairSyntax.dest_pabs abs_spec; value
/seL4-l4v-10.1.1/HOL4/src/datatype/
H A Dind_types.sml459 val pv = lhand(body(rator(rand bimp))) value
/seL4-l4v-10.1.1/HOL4/src/num/reduce/src/
H A DArithconv.sml225 val pv = mk_var {Name= "p", Ty=num} value
/seL4-l4v-10.1.1/HOL4/src/ring/src/
H A Dabstraction.sml65 val pv = filter (C mem fvrhs) (!fv_ass) value

Completed in 150 milliseconds