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 DunifyTools.sml161 else if is_var tm1 then
168 else if is_var tm2 then solve' sub ((bvs2, tm2), (bvs1, tm1)) rest
H A Dho_basicTools.sml74 if is_var tm andalso not (is_bv bvs tm) then
/seL4-l4v-10.1.1/HOL4/examples/HolBdd/
H A DPrimitiveBddRules.sml137 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 DCooperMath.sml535 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 DIntDP_Munge.sml71 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 DrealSimps.sml392 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 Dres_quanLib.sml486 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 Dhh_write.ml87 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 DcompilerLib.sml87 | 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 Dreg_allocLib.sml99 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 Dm0_core_decompLib.sml40 SOME (v, _) => not (Term.is_var v)
/seL4-l4v-10.1.1/HOL4/src/0/
H A DNet.sml59 if is_bvar tm orelse is_var tm then V else
/seL4-l4v-10.1.1/HOL4/src/Boolify/src/
H A DEncode.sml86 in (Rator=f) andalso is_var Rand andalso (type_of Rand = ty)
/seL4-l4v-10.1.1/HOL4/src/HolSat/
H A Ddpll.sml110 in if is_var y then subst [x|->y] l
H A DminisatProve.sml47 in if is_var y then subst [x|->y] l
/seL4-l4v-10.1.1/HOL4/src/datatype/
H A DDataSize.sml62 in (Rator=f) andalso is_var Rand andalso (type_of Rand = ty)
/seL4-l4v-10.1.1/HOL4/src/experimental-kernel/
H A DNet.sml56 if is_var tm then V else
/seL4-l4v-10.1.1/HOL4/src/monad/
H A Dparmonadsyntax.sml155 NONE => if is_var f then #1 (dest_var f)
/seL4-l4v-10.1.1/HOL4/src/parse/
H A DAbsyn.sml125 if Term.is_var tm
/seL4-l4v-10.1.1/HOL4/src/pattern_matches/
H A DconstrFamiliesLib.sml582 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 DPGspec.sml233 else if is_var res
/seL4-l4v-10.1.1/HOL4/src/quantHeuristics/
H A DquantHeuristicsLibAbbrev.sml29 not ((is_var t) orelse (is_const t))
/seL4-l4v-10.1.1/HOL4/src/tfl/src/
H A DRW.sml78 * 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 DtailrecLib.sml28 val _ = every (fn x => every is_var (list_dest dest_conj x)) zs
/seL4-l4v-10.1.1/HOL4/examples/pgcl/src/
H A DwpTools.sml123 val _ = is_var la orelse raise ERR "dest_lam" "lhs rator not var"

Completed in 295 milliseconds

12345678