Searched refs:is_var (Results 26 - 50 of 178) sorted by relevance

12345678

/seL4-l4v-10.1.1/HOL4/src/holyhammer/legacy/
H A Dhh_tac.ml126 if is_var hop then if mem hop bnd then (cmin, vmin)
143 if is_var op then try assoc (fst (dest_var op)) vmin with _ -> 0 else failwith "fol_conv_assoc";;
253 if is_var tm then sofar else fn (dest_const tm) sofar;;
346 else if is_var tm || is_const tm then failwith "find_lambda"
355 else if is_var tm || is_const tm then rEFL tm else
388 else if is_var tm || is_const tm then failwith "find_lambda"
397 else if is_var tm || is_const tm then rEFL tm else
/seL4-l4v-10.1.1/HOL4/src/tfl/src/
H A DInduction.sml110 (is_var l1 andalso is_var l2)
180 (all is_var col_i) orelse
181 (all (fn p => Literal.is_literal p orelse is_var p) col_i) orelse
182 (all (fn p => not (Literal.is_pure_literal p) andalso not (is_var p)) col_i)
207 if all is_var col0 (* column 0 is all variables *)
215 val (litpats, varpats) = Lib.partition (not o is_var) lits
332 val globals = (if is_var R then [R] else [])@pat_vars@SV
469 fun var_pure theta = Lib.all (fn {redex,residue} => is_var residue) theta;
574 in if is_var t
[all...]
/seL4-l4v-10.1.1/HOL4/examples/dev/Fact32/
H A Dexor32.ml89 andalso all is_var (strip_pair(rand tm))
/seL4-l4v-10.1.1/HOL4/src/combin/
H A DcombinSyntax.sml103 if is_var s then (f,fst(dest_var s),args)
/seL4-l4v-10.1.1/HOL4/examples/machine-code/just-in-time/
H A Dexport_codeLib.sml15 val vs = map (fn (x,y) => (if is_var x then ``0:num`` else cdr (cdr x),y)) vs
/seL4-l4v-10.1.1/HOL4/examples/machine-code/lisp/
H A Dexport_codeLib.sml15 val vs = map (fn (x,y) => (if is_var x then ``0:num`` else cdr (cdr x),y)) vs
/seL4-l4v-10.1.1/HOL4/examples/theorem-prover/lisp-runtime/implementation/
H A Dexport_codeLib.sml18 val vs = map (fn (x,y) => (if is_var x then ``0:num`` else
/seL4-l4v-10.1.1/HOL4/src/integer/
H A DintSimps.sml103 if is_var tm then true
240 | NONE => if is_var t then if HOLset.member(bnds, t) then acc
/seL4-l4v-10.1.1/HOL4/src/new-datatype/
H A DWitness.sml59 fun is_lit x = (is_const x) orelse (is_var x);
70 else if is_var tm then
/seL4-l4v-10.1.1/HOL4/src/num/arith/src/
H A DGen_arith.sml40 if (is_var tm) then true
110 fun is_num_var tm = is_var tm andalso type_of tm = num_ty
H A DnumSimps.sml438 | NONE => if is_var t then if HOLset.member(bnds, t) then acc
548 val lsucs = find_terms (fn t => is_suc t andalso is_var (rand t)) l
573 val lsucs = find_terms (fn t => is_suc t andalso is_var (rand t)) l
574 val v = rand (valOf (List.find (is_var o rand) lsucs))
/seL4-l4v-10.1.1/HOL4/src/simp/src/
H A DOpening.sml104 (if (is_var (rand tm) andalso mem (rand tm) genvars)
139 fun reprocess_flag assum = if is_var assum then false else true;
H A DCond_rewr.sml303 not (is_var t) orelse type_of t <> bool orelse
330 else if is_var n andalso not (n IN hypfvs) then
359 else if is_var conc andalso not (conc IN hypfvs) then
/seL4-l4v-10.1.1/HOL4/examples/misc/
H A DwardScript.sml234 listSyntax.is_nil res2 andalso List.all is_var pfx1 andalso
235 List.all is_var sfx1
/seL4-l4v-10.1.1/HOL4/examples/dev/sw2/
H A DregAlloc.sml68 (* is_var exp andalso *)
162 if is_var x then (x |-> find_pos (regenv, x)) :: ys
220 if is_var x then (x |-> find_reg (regenv, x)) :: ys
274 if is_var exp
464 else if is_var M andalso is_mem M then
H A Dbasic.sml29 is_var t orelse is_word_literal t orelse
/seL4-l4v-10.1.1/HOL4/src/postkernel/
H A DHolKernel.sml510 if is_var vtm then let
541 if is_var vhop andalso not (HOLset.member (lconsts, vhop)) andalso
586 val (realinsts, patterns) = partition (is_var o #redex) insts
660 if is_var vtm then
697 (if is_var p then p
/seL4-l4v-10.1.1/HOL4/examples/lambda/basics/
H A DbinderLib.sml159 if is_var t then
167 val strings = List.filter (fn t => is_var t orelse is_string_literal t)
169 val stringsets = List.filter is_var (find_terms (eqty stringset_ty) t)
186 fun filterthis t = not (is_var t) orelse mem t finite_sets
314 case List.find (not o is_var) args of
/seL4-l4v-10.1.1/HOL4/src/coretypes/
H A DpairLib.sml120 if is_var vs
/seL4-l4v-10.1.1/HOL4/src/holyhammer/
H A DhhTptp.sml41 else if is_var tm then tptp_of_var arity tm
/seL4-l4v-10.1.1/HOL4/src/metis/
H A DmlibTerm.sig33 val is_var : term -> bool value
/seL4-l4v-10.1.1/HOL4/src/prekernel/
H A DFinalTerm-sig.sml49 val is_var : term -> bool value
/seL4-l4v-10.1.1/HOL4/src/tactictoe/src/
H A DtttTools.sml360 else if is_var t1 andalso is_var t2 then Term.compare (t1,t2)
361 else if is_var t1 then LESS
362 else if is_var t2 then GREATER
/seL4-l4v-10.1.1/HOL4/examples/machine-code/x64_compiler/
H A Dx64_compilerLib.sml84 | ends (FUN_VAL t) = if is_var t orelse pairSyntax.is_pair t then [t] else []
/seL4-l4v-10.1.1/HOL4/examples/machine-code/instruction-set-models/ppc/
H A Dprog_ppcLib.sml52 val mems = filter (is_var o cdr o cdr) mems
99 fun g th tm tm' = if is_var tm then INST [ tm |-> tm' ] th else th

Completed in 194 milliseconds

12345678