Searched refs:is_var (Results 126 - 150 of 178) sorted by relevance

12345678

/seL4-l4v-10.1.1/HOL4/examples/HolCheck/
H A DbddTools.sml206 in List.map (fn v => if is_var v then T else v) t1 end;
H A DcommonTools.sml148 fun is_bool_var v = is_var v andalso (Type.compare(type_of v,bool)=EQUAL)
H A DlzConv.sml458 if is_var arg_t then
1292 if not(is_var v)
1404 if not(is_var x)
/seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/common/
H A DutilsLib.sml364 SOME v => if Term.is_var v andalso not (Term.var_occurs v tm2)
376 else if Term.is_var l andalso not (Term.var_occurs l r)
H A Dcore_decompilerLib.sml79 SOME (v, _) => not (Term.is_var v)
/seL4-l4v-10.1.1/HOL4/src/IndDef/
H A DInductiveDefinition.sml644 andalso all is_var (snd(strip_comb tm))
695 if is_var(hd schem) then (clauses,[])
/seL4-l4v-10.1.1/HOL4/src/coretypes/
H A DpairScript.sml796 S " | check (h::t) = is_var h andalso not(mem h t) andalso check t", NL,
806 S " if is_var vstruct then Term.mk_abs(vstruct, body)", NL,
/seL4-l4v-10.1.1/graph-refine/
H A Dpseudo_compile.py303 if not v.is_var (lv)]
/seL4-l4v-10.1.1/HOL4/examples/machine-code/instruction-set-models/arm/
H A Dprog_armLib.sml187 val v = hd (filter (is_var) ys @ ys)
273 val v = hd (filter (is_var) ys @ ys)
/seL4-l4v-10.1.1/HOL4/examples/ARM/v7/
H A Darm_disassemblerLib.sml180 if Term.is_var tm then
801 val v2 = opt (is_var cond orelse is_PC cond) "2"
/seL4-l4v-10.1.1/HOL4/examples/HolBdd/
H A DDerivedBddRules.sml154 if is_var tm
159 if is_var tm' then BddVar false vm tm' else BddNot(recfn tm')
/seL4-l4v-10.1.1/HOL4/examples/dev/
H A Dcompile.sml139 else if null(free_vars t) orelse is_var t
497 is_var tm
1198 if is_var t then applysubst theta t else
1374 if is_var vs
1554 else if is_var bdy andalso can (assoc bdy) args_match
/seL4-l4v-10.1.1/HOL4/src/parse/
H A Dterm_pp.sml770 if (is_pair tm orelse is_var tm) then
1641 fun is_atom tm = is_const tm orelse is_var tm
1792 else if is_var f then pr_atomf (f, args @ [Rand])
H A DOverload.sml445 if is_var realf andalso
/seL4-l4v-10.1.1/HOL4/src/temporal/src/
H A DtemporalLib.sml888 if (is_var t) then []
960 if (is_var t) then []
1228 in if (is_var x) then #Name(dest_var f)
/seL4-l4v-10.1.1/HOL4/examples/dev/sw/
H A DANF.sml136 else if is_var t orelse is_word_literal t orelse numSyntax.is_numeral t orelse is_const t
H A DIR.sml189 if is_var exp then
/seL4-l4v-10.1.1/HOL4/examples/dev/sw/working/0.1/
H A DANF.sml136 else if is_var t orelse is_word_literal t orelse numSyntax.is_numeral t orelse is_const t
/seL4-l4v-10.1.1/HOL4/examples/dev/sw/working/0.2/
H A DANF.sml136 else if is_var t orelse is_word_literal t orelse numSyntax.is_numeral t orelse is_const t
/seL4-l4v-10.1.1/HOL4/examples/elliptic/c_output/
H A Dc_outputLib.sml297 else if (is_var exp) then
/seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/arm8/step/
H A Darm8_stepLib.sml706 val vs = List.filter Term.is_var o fst o listSyntax.dest_list o fst o
/seL4-l4v-10.1.1/HOL4/src/datatype/record/
H A DRecordType.sml56 fun name_of tm = if is_var tm then SOME (fst(dest_var tm)) else NONE
/seL4-l4v-10.1.1/HOL4/src/num/termination/
H A DTotalDefn.sml500 | SOME R => is_var R;
/seL4-l4v-10.1.1/HOL4/src/pfl/
H A Dindex.sml154 if is_var tm orelse is_const tm then mk_some tm else
/seL4-l4v-10.1.1/HOL4/src/quotient/examples/
H A Dind_rel.sml224 if is_var tm then member tm relations else
475 if is_var tm then member tm relations else
901 if is_var tm then false else
1630 if is_var tm then member tm prop_vars else

Completed in 205 milliseconds

12345678