Searched refs:is_var (Results 51 - 75 of 178) sorted by relevance
12345678
/seL4-l4v-10.1.1/HOL4/examples/miller/ho_prover/ |
H A D | unifyTools.sml | 161 else if is_var tm1 then 168 else if is_var tm2 then solve' sub ((bvs2, tm2), (bvs1, tm1)) rest
|
H A D | ho_basicTools.sml | 74 if is_var tm andalso not (is_bv bvs tm) then
|
/seL4-l4v-10.1.1/HOL4/examples/HolBdd/ |
H A D | PrimitiveBddRules.sml | 137 if is_var v andalso type_of v = bool 270 if not(is_var v) 273 if not(is_var v') 339 if is_var v andalso Varmap.eq(vm,vm1) andalso Varmap.eq(vm1,vm2) 373 if not(is_var v) 468 if not(is_var v)
|
/seL4-l4v-10.1.1/HOL4/src/integer/ |
H A D | CooperMath.sml | 535 fun Munge t = if is_var t then REWR_CONV (GSYM INT_MUL_LID) t 549 if is_var t0 then 567 if is_mult tm andalso not (is_var (rand tm)) then let 569 val (var, rest) = Lib.pluck is_var mcands 710 List.mapPartial (fn a => if is_var (rand a) then
|
H A D | IntDP_Munge.sml | 71 else if is_var tm andalso type_of tm = int_ty then [] 111 else if is_var tm then empty_tmset 169 if is_var bv then mk_forall(bv, t)
|
/seL4-l4v-10.1.1/HOL4/src/real/ |
H A D | realSimps.sml | 392 if is_var tm then true 430 fun is_num_var tm = is_var tm andalso type_of tm = real_ty 558 | NONE => if is_var t then if HOLset.member(bnds, t) then acc
|
/seL4-l4v-10.1.1/HOL4/src/res_quan/src/ |
H A D | res_quanLib.sml | 486 if is_var tm 508 if is_var tm then [tm] else 529 if is_var left then rightty
|
/seL4-l4v-10.1.1/HOL4/src/holyhammer/legacy/ |
H A D | hh_write.ml | 87 if Hashtbl.mem cs tm || is_var tm then () else 106 if is_var tm then 195 if is_var tm then begin 503 let tys tm = map type_of (find_terms (fun x -> is_var x || is_const x) tm) in 561 if is_var tm then begin 576 if is_var tm then os oc (Tmm.find tm bnd)
|
/seL4-l4v-10.1.1/HOL4/examples/machine-code/compiler/ |
H A D | compilerLib.sml | 87 | ends (FUN_VAL t) = if is_var t orelse pairSyntax.is_pair t then [t] else [] 194 val xs1 = find_terms (fn x => is_comb x andalso is_var (car x) andalso
|
H A D | reg_allocLib.sml | 99 val t = find_term (fn x => is_compilable x andalso not (is_var x)) rhs 103 find_term (fn v => is_var v andalso (ty = type_of v)) t 338 if is_var x andalso is_var y then (x,y)::pref t else pref t
|
/seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/m0/decompiler/ |
H A D | m0_core_decompLib.sml | 40 SOME (v, _) => not (Term.is_var v)
|
/seL4-l4v-10.1.1/HOL4/src/0/ |
H A D | Net.sml | 59 if is_bvar tm orelse is_var tm then V else
|
/seL4-l4v-10.1.1/HOL4/src/Boolify/src/ |
H A D | Encode.sml | 86 in (Rator=f) andalso is_var Rand andalso (type_of Rand = ty)
|
/seL4-l4v-10.1.1/HOL4/src/HolSat/ |
H A D | dpll.sml | 110 in if is_var y then subst [x|->y] l
|
H A D | minisatProve.sml | 47 in if is_var y then subst [x|->y] l
|
/seL4-l4v-10.1.1/HOL4/src/datatype/ |
H A D | DataSize.sml | 62 in (Rator=f) andalso is_var Rand andalso (type_of Rand = ty)
|
/seL4-l4v-10.1.1/HOL4/src/experimental-kernel/ |
H A D | Net.sml | 56 if is_var tm then V else
|
/seL4-l4v-10.1.1/HOL4/src/monad/ |
H A D | parmonadsyntax.sml | 155 NONE => if is_var f then #1 (dest_var f)
|
/seL4-l4v-10.1.1/HOL4/src/parse/ |
H A D | Absyn.sml | 125 if Term.is_var tm
|
/seL4-l4v-10.1.1/HOL4/src/pattern_matches/ |
H A D | constrFamiliesLib.sml | 582 if (is_var p andalso mem p vs) then 639 val _ = if List.all (fn (vs, c) => is_var c andalso Lib.mem c vs) col then 827 (if is_var c then (tl, ts) else failwith "" "extract_literal") 922 (if is_var c then ts else failwith "" "extract_literal")
|
/seL4-l4v-10.1.1/HOL4/src/pred_set/src/ |
H A D | PGspec.sml | 233 else if is_var res
|
/seL4-l4v-10.1.1/HOL4/src/quantHeuristics/ |
H A D | quantHeuristicsLibAbbrev.sml | 29 not ((is_var t) orelse (is_const t))
|
/seL4-l4v-10.1.1/HOL4/src/tfl/src/ |
H A D | RW.sml | 78 * in if is_var head then can (find_term (aconv head)) else fn _ => false 83 * in if is_var head then can (find_term (can (match_term tm))) 95 in if is_var head then alike head tm else K false 281 local fun sys_var tm = (is_var tm andalso
|
/seL4-l4v-10.1.1/HOL4/examples/machine-code/hoare-triple/ |
H A D | tailrecLib.sml | 28 val _ = every (fn x => every is_var (list_dest dest_conj x)) zs
|
/seL4-l4v-10.1.1/HOL4/examples/pgcl/src/ |
H A D | wpTools.sml | 123 val _ = is_var la orelse raise ERR "dest_lam" "lhs rator not var"
|
Completed in 295 milliseconds
12345678