/seL4-l4v-10.1.1/HOL4/src/datatype/mutrec/ |
H A D | Recftn.sml | 121 if is_var tm then 257 andalso (is_var constructor) 659 if is_var constructor then
|
/seL4-l4v-10.1.1/HOL4/src/integer/ |
H A D | OmegaMath.sml | 349 else if is_mult (rand tm) andalso not (is_var (rand (rand tm))) then 356 else if is_mult tm andalso not (is_var (rand tm)) then 526 is_int_literal c andalso is_var v andalso
|
/seL4-l4v-10.1.1/HOL4/examples/machine-code/graph/ |
H A D | derive_specsLib.sml | 209 (if tm |> rator |> is_var then REWR_CONV (GSYM READ8_def) tm 436 is_var (rand tm)) c 527 in is_var v end;
|
H A D | exportLib.sml | 230 val cs = filter is_var (list_dest dest_comb pat)
|
/seL4-l4v-10.1.1/HOL4/examples/machine-code/instruction-set-models/x86_64/ |
H A D | prog_x64Lib.sml | 168 val v = hd (filter (is_var) ys @ ys) 229 val v = hd (filter (is_var) ys @ ys) 324 val v = hd (filter (is_var) ys @ ys)
|
/seL4-l4v-10.1.1/HOL4/examples/miller/useful/ |
H A D | HurdUseful.sml | 563 fun is_tmvar ((tmvars, _) : vars) tm = is_var tm andalso mem tm tmvars; 599 val _ = assert (is_var tm) (ERR "dest_bv" "not a var") 850 if is_var v andalso all (not o free_in v) (checked @ rest) then
|
/seL4-l4v-10.1.1/HOL4/examples/machine-code/hoare-triple/ |
H A D | helperLib.sml | 612 fun frame_var tm = is_var tm andalso not (mem tm fixed_vars) 1083 in if is_var x then 0 1235 val tm = hd (filter (fn tm => is_eq tm andalso is_var(cdr tm)) hs) 1238 val tm = hd (filter (fn tm => is_eq tm andalso is_var((cdr o car) tm) andalso (free_vars (cdr tm) = [])) hs) 1261 fun frame_var tm = is_var tm andalso not (mem tm fixed_vars)
|
/seL4-l4v-10.1.1/HOL4/src/pattern_matches/ |
H A D | patternMatchesLib.sml | 386 val _ = if is_var a andalso free_in a x then () else failwith "case-split on non pattern var" 1193 val _ = if (is_var tt_col) then () else failwith "no var" 1443 val nv_parts_vars = filter (fn (v, n) => is_var n) (zip (List.rev res_l) nv_parts) 1478 andalso is_var (subst pat_vars_s0 (#redex vp))) new_col_subst 1941 if (is_var p andalso mem p vs) then 0 else 1); 1945 | ((vs, p) :: _) => if (is_var p andalso mem p vs) then 0 else 1959 | aux n ((vs, p) :: pL) = if (is_var p) 1981 not (is_var p andalso mem p vs)) rows; 2382 if (Term.is_var p) andalso List.exists (aconv p) vs then 2404 val cols''' = filter (fn (_, ps) => not (List.all (fn (vs, p) => is_var [all...] |
/seL4-l4v-10.1.1/HOL4/src/quantHeuristics/ |
H A D | quantHeuristicsLibBase.sml | 1269 val i_ok = is_var i orelse 1272 in (type_of i_v = unit_ty) andalso (is_var i_b) end 1275 val tL_simple = all (fn tx => is_var tx orelse 1277 in (tx_v = v) andalso (is_var tx_b) end) tL 1552 if is_var i then 1564 else if (is_var (snd (dest_abs i)) handle HOL_ERR _ => false) then
|
/seL4-l4v-10.1.1/HOL4/src/metis/ |
H A D | normalForms.sml | 897 if is_var v andalso all (not o free_in v) (def :: checked @ rest) then 1152 op_mem aconv redex vs andalso (type_of redex <> bool orelse is_var residue); 1181 not let val (t,ws) = strip_comb tm in is_var t andalso subset ws vs end;
|
/seL4-l4v-10.1.1/HOL4/examples/ARM/v7/ |
H A D | arm_encoderLib.sml | 482 if is_var cond orelse is_AL cond then 876 if is_var cond orelse is_AL cond then 1441 (mk_word4 (if is_var cond orelse is_PC cond then 15 else 14),i)
|
/seL4-l4v-10.1.1/HOL4/examples/dev/sw/working/0.1/ |
H A D | IR.sml | 180 if is_var exp then
|
/seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/mips/prog/ |
H A D | mips_progLib.sml | 256 [v] => if Term.is_var v
|
/seL4-l4v-10.1.1/HOL4/src/1/ |
H A D | Mutual.sml | 97 if ((is_var body) orelse (is_const body))
|
H A D | boolSyntax.sml | 274 if all is_var args
|
/seL4-l4v-10.1.1/HOL4/src/compute/src/ |
H A D | clauses.sml | 36 else if (is_var t)
|
/seL4-l4v-10.1.1/HOL4/src/datatype/ |
H A D | ind_types.sml | 83 if is_var tm then insert tm acc 795 map (fn t => mk_abs(find_term is_var t,t)) bods 859 if is_var a then (g,g) 1471 filter (fn t => List.exists (not o is_var)
|
/seL4-l4v-10.1.1/HOL4/src/holyhammer/ |
H A D | hhTranslate.sml | 124 if is_const tm orelse is_var tm then update_adict adict 0 tm
|
H A D | hhWriter.sml | 192 if is_var tm then os oc (dfind_err "var" tm (!(#var_names state)))
|
/seL4-l4v-10.1.1/HOL4/src/parse/ |
H A D | FCNet.sml | 341 | SOME i => if is_var t2 andalso
|
/seL4-l4v-10.1.1/HOL4/src/postkernel/ |
H A D | TheoryPP.sml | 185 fun is_atom t = Term.is_var t orelse Term.is_const t
|
/seL4-l4v-10.1.1/HOL4/src/rational/ |
H A D | fracLib.sml | 328 if is_var top_rator orelse top_rator=``rep_rat`` then
|
/seL4-l4v-10.1.1/HOL4/src/tactictoe/src/ |
H A D | tttSynt.sml | 153 fun is_varconst x = is_var x orelse is_const x
|
/seL4-l4v-10.1.1/graph-refine/ |
H A D | syntax.py | 438 def is_var (self, (nm, typ)): member in class:Expr 610 if not v.is_var (lv)]
|
/seL4-l4v-10.1.1/HOL4/examples/theorem-prover/milawa-prover/ |
H A D | milawa_initScript.sml | 112 val _ = is_var x orelse fail() in (x,y) end
|