Searched refs:is_var (Results 101 - 125 of 178) sorted by relevance

12345678

/seL4-l4v-10.1.1/HOL4/src/datatype/mutrec/
H A DRecftn.sml121 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 DOmegaMath.sml349 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 Dderive_specsLib.sml209 (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 DexportLib.sml230 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 Dprog_x64Lib.sml168 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 DHurdUseful.sml563 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 DhelperLib.sml612 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 DpatternMatchesLib.sml386 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 DquantHeuristicsLibBase.sml1269 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 DnormalForms.sml897 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 Darm_encoderLib.sml482 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 DIR.sml180 if is_var exp then
/seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/mips/prog/
H A Dmips_progLib.sml256 [v] => if Term.is_var v
/seL4-l4v-10.1.1/HOL4/src/1/
H A DMutual.sml97 if ((is_var body) orelse (is_const body))
H A DboolSyntax.sml274 if all is_var args
/seL4-l4v-10.1.1/HOL4/src/compute/src/
H A Dclauses.sml36 else if (is_var t)
/seL4-l4v-10.1.1/HOL4/src/datatype/
H A Dind_types.sml83 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 DhhTranslate.sml124 if is_const tm orelse is_var tm then update_adict adict 0 tm
H A DhhWriter.sml192 if is_var tm then os oc (dfind_err "var" tm (!(#var_names state)))
/seL4-l4v-10.1.1/HOL4/src/parse/
H A DFCNet.sml341 | SOME i => if is_var t2 andalso
/seL4-l4v-10.1.1/HOL4/src/postkernel/
H A DTheoryPP.sml185 fun is_atom t = Term.is_var t orelse Term.is_const t
/seL4-l4v-10.1.1/HOL4/src/rational/
H A DfracLib.sml328 if is_var top_rator orelse top_rator=``rep_rat`` then
/seL4-l4v-10.1.1/HOL4/src/tactictoe/src/
H A DtttSynt.sml153 fun is_varconst x = is_var x orelse is_const x
/seL4-l4v-10.1.1/graph-refine/
H A Dsyntax.py438 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 Dmilawa_initScript.sml112 val _ = is_var x orelse fail() in (x,y) end

Completed in 235 milliseconds

12345678