Searched defs:aux (Results 1 - 25 of 31) sorted by relevance

12

/seL4-l4v-10.1.1/HOL4/examples/acl2/tests/inputs/
H A Drecords.lisp[all...]
H A Dltl.lisp
H A Dcircuits.lisp
H A Dcircuit-bisim.lisp
/seL4-l4v-10.1.1/HOL4/examples/machine-code/graph/
H A Dcond_cleanLib.sml106 fun aux [] result = result function
H A DwriterLib.sml14 fun aux (#"_"::cs) = aux cs | aux xs = String.implode (rev xs) function
H A DbackgroundLib.sml98 fun aux k n [] = fail() function
H A Dderive_specsLib.sml73 fun aux t [] = t function
105 fun aux (p:int) (seen:int list) (guard:term) = function
/seL4-l4v-10.1.1/HOL4/src/HolSmt/
H A DSmtLib_Parser.sml176 fun aux acc = function
219 fun aux acc = function
H A DSmtLib_Theories.sml60 fun aux t [] = raise Match (* should never happen *) function
71 fun aux t [] = t function
81 fun aux function
[all...]
H A DZ3_ProofReplay.sml443 fun aux (dict, t) = function
/seL4-l4v-10.1.1/HOL4/src/simp/src/
H A DOpening.sml68 fun aux tm = if is_congruence tm then #1 (dest_binop tm) function
75 fun aux tm = if is_congruence tm then 0 else aux (snd(dest_imp tm)) + 1 function
/seL4-l4v-10.1.1/HOL4/examples/acl2/lisp/
H A Dpkg-alist-to-alist.lisp
/seL4-l4v-10.1.1/HOL4/src/1/
H A DPmatchHeuristics.sml44 fun aux a rowL = if (length (hd rowL) = 0) then List.rev a else function
81 let fun aux n [] = n function
187 fun aux () = case (!hL_ref) of function
H A DPmatch.sml472 fun aux min = case (heu_fun ()) of function
/seL4-l4v-10.1.1/HOL4/src/datatype/
H A DDatatypeSimps.sml43 fun aux res n m avoid ty = let function
/seL4-l4v-10.1.1/HOL4/examples/machine-code/compiler/
H A DcodegenLib.sml417 fun aux [] ys zs = ([],rev ys,zs) function
H A Dreg_allocLib.sml162 fun aux tm = let function
199 val aux = filter (fn (lhs,rhs) => not (mem x (free_vars rhs))) aux value
/seL4-l4v-10.1.1/HOL4/examples/machine-code/instruction-set-models/arm/
H A Dprog_armLib.sml49 fun aux v = let val m = match_term tm (car (car v)) in (snd o process o cdr o car) v end function
/seL4-l4v-10.1.1/HOL4/examples/machine-code/x64_compiler/
H A Dx64_codegenLib.sml316 fun aux [] ys zs = ([],rev ys,zs) function
/seL4-l4v-10.1.1/seL4/src/arch/arm/machine/
H A Dl2c_310.c252 uint32_t aux; local
/seL4-l4v-10.1.1/HOL4/examples/elliptic/
H A DUseful.sml253 fun aux _ res _ [] = res function
265 fun aux res l 0 = (rev res, l) function
[all...]
/seL4-l4v-10.1.1/HOL4/src/metis/
H A DmlibUseful.sml206 fun aux _ res _ [] = res function
218 fun aux res l 0 = (rev res, l) function
[all...]
/seL4-l4v-10.1.1/HOL4/src/pattern_matches/
H A DpatternMatchesSyntax.sml42 fun aux acc l = function
160 fun aux acc t = let function
455 fun aux acc v col_no = if (col_no <= 1) then List.rev (v::acc) else ( function
[all...]
/seL4-l4v-10.1.1/HOL4/examples/theorem-prover/lisp-runtime/extract/
H A Dlisp_extractLib.sml166 fun aux tm = function

Completed in 173 milliseconds

12