Searched refs:is_var (Results 76 - 100 of 178) sorted by relevance

12345678

/seL4-l4v-10.1.1/HOL4/examples/ARM/v7/
H A DarmLib.sml70 fun fix_condition tm = if is_var tm then condition_to_word4 tm else tm
H A Darm_parserLib.sml758 (is_var tm orelse word_lower_same (tm,mk_word4 7));
1735 if is_var i then
1777 if is_var i then
1785 if is_var cond orelse is_AL cond then
1789 val wide_okay = if is_var cond orelse is_AL cond then
1822 (if is_var i then
1841 if is_var i then
1881 (if is_var i then
1903 (if is_var i then
1951 if is_var
[all...]
/seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/common/
H A DstateLib.sml672 Term.is_var redex andalso is_ok_rhs residue andalso
686 |> List.partition (Term.is_var o #residue)
1296 Term.is_var tm orelse
1298 SOME (p, i) => Term.is_var p andalso is_word_lit i
1301 SOME (p, i) => Term.is_var p andalso is_word_lit i
1589 if Term.is_var a then SOME (a |-> b)
1639 val frees = List.filter Term.is_var o explode_reg
/seL4-l4v-10.1.1/HOL4/src/experimental-kernel/
H A DTerm.sml107 fun is_var (Var _) = true | is_var _ = false function
195 if is_var v then Abs(v, body)
687 else if List.all (is_var o #redex) theta then let
932 | SOME i => if is_var tm andalso
/seL4-l4v-10.1.1/HOL4/src/1/
H A DPrim_rec.sml50 in if is_var Rand then pull_off_var Rator (Rand::acc) else (tm, acc)
95 val (vars, others) = partition is_var patargs
210 let val args' = uncurry (C (curry op@)) (Lib.partition is_var args)
234 val oxargs = map (uncurry (C (curry op@)) o Lib.partition is_var) uxargs
480 if is_var body orelse is_const body then REFL else
952 val vars = filter is_var args
H A DTactic.sml243 * if not(is_var x') then failwith X_GEN_TAC else *
257 if is_var x1
994 val _ = is_var Pvar
/seL4-l4v-10.1.1/HOL4/examples/acl2/ml/
H A DfunctionEncodeLib.sml133 orelse (is_var ratort andalso
152 else if (is_var ratort andalso
1275 is_var (RHS (concl thm))
1631 else if is_var f1 andalso is_var f2
1752 if all (all is_var o snd o strip_comb) constructors andalso
1820 val _ = if is_var a then () else
2090 val _ = if exists (not o is_var) vars then
2121 if is_var term then mk_var(fst (dest_var term),t) else raise e;
2472 (is_var
[all...]
/seL4-l4v-10.1.1/HOL4/examples/dev/
H A Dvsynth.sml274 andalso all is_var (strip_pair(rand tm))
299 andalso is_var (rand tm);
/seL4-l4v-10.1.1/HOL4/src/metis/
H A DfolTools.sml186 val varnames = matchTools.vfree_names is_var o list_mk_conj';
366 fun is_skol v = is_var v andalso mem (fst (dest_var v)) skols
H A DmlibTerm.sml44 val is_var = can dest_var; value
249 if is_var tm orelse is_const tm then basic tm else pp_btm tm
/seL4-l4v-10.1.1/HOL4/examples/machine-code/decompiler/
H A DdecompilerLib.sml197 fst (dest_var (find_term is_var tm)) handle HOL_ERR e =>
222 if (is_var (cdr tm) andalso
233 |> filter (fn tm => (is_var o rand) tm handle HOL_ERR _ => false)
1006 if is_var tm andalso type_of tm = ``:bool`` then SPEC tm GUARD_T else
1007 if is_neg tm andalso is_var (cdr tm ) then SPEC (cdr tm) GUARD_F
1014 if is_var tm then tagged_var_to_num tm else
1015 if is_neg tm andalso is_var (cdr tm) then tagged_var_to_num (cdr tm) else
1201 val _ = every (fn x => every is_var (list_dest dest_conj x)) zs
/seL4-l4v-10.1.1/HOL4/examples/separationLogic/src/
H A Dvars_as_resourceBaseFunctor.sml743 val turn = (is_var r) andalso (not (is_var l))
/seL4-l4v-10.1.1/HOL4/examples/dev/sw/working/0.2/
H A DACF.sml110 if is_var t orelse is_word_literal t orelse numSyntax.is_numeral t orelse is_const t orelse is_pair t then
H A DIR.sml180 if is_var exp then
/seL4-l4v-10.1.1/HOL4/examples/elliptic/
H A Delliptic_exampleScript.sml349 not (is_var x) andalso
/seL4-l4v-10.1.1/HOL4/src/0/
H A DTerm.sml120 fun is_var (Fv _) = true | is_var _ = false; function
552 is_var redex andalso b)
625 => if not (all is_var vlist) then raise ERR "list_mk_binder" ""
/seL4-l4v-10.1.1/HOL4/src/HolQbf/
H A DQDimacs.sml50 if Term.is_var tm then
/seL4-l4v-10.1.1/HOL4/src/coretypes/
H A DPairedLambda.sml171 if is_var body orelse is_const body
H A DpairSyntax.sml348 if is_pair l orelse is_var l
/seL4-l4v-10.1.1/HOL4/src/marker/
H A DmarkerLib.sml116 if (is_var t orelse is_const t) andalso not (!match_var_or_const)
/seL4-l4v-10.1.1/HOL4/src/num/
H A DnumLib.sml351 if is_var v then
/seL4-l4v-10.1.1/HOL4/src/postkernel/
H A DSharingTables.sml194 if is_var tm then let
/seL4-l4v-10.1.1/HOL4/examples/lambda/barendregt/
H A DreductionEval.sml293 fun filterthis t = not (is_var t) orelse mem t finite_sets
/seL4-l4v-10.1.1/HOL4/examples/diningcryptos/
H A DformalizeUseful.sml621 fun is_tmvar ((tmvars, _) : vars) tm = is_var tm andalso mem tm tmvars;
657 val _ = assert (is_var tm) (ERR "dest_bv" "not a var")
907 if is_var v andalso all (not o free_in v) (checked @ rest) then
H A DsubtypeUseful.sml619 fun is_tmvar ((tmvars, _) : vars) tm = is_var tm andalso mem tm tmvars;
655 val _ = assert (is_var tm) (ERR "dest_bv" "not a var")
913 if is_var v andalso all (not o free_in v) (checked @ rest) then

Completed in 396 milliseconds

12345678