Searched refs:is_var (Results 1 - 25 of 178) sorted by path
12345678
/seL4-l4v-10.1.1/HOL4/examples/ARM/v7/ |
H A D | armLib.sml | 70 fun fix_condition tm = if is_var tm then condition_to_word4 tm else tm
|
H A D | arm_disassemblerLib.sml | 180 if Term.is_var tm then 801 val v2 = opt (is_var cond orelse is_PC cond) "2"
|
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)
|
H A D | arm_parserLib.sml | 758 (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/HolBdd/ |
H A D | DerivedBddRules.sml | 154 if is_var tm 159 if is_var tm' then BddVar false vm tm' else BddNot(recfn tm')
|
H A D | PrimitiveBddRules.sml | 137 if is_var v andalso type_of v = bool 270 if not(is_var v) 273 if not(is_var v') 339 if is_var v andalso Varmap.eq(vm,vm1) andalso Varmap.eq(vm1,vm2) 373 if not(is_var v) 468 if not(is_var v)
|
/seL4-l4v-10.1.1/HOL4/examples/HolCheck/ |
H A D | bddTools.sml | 206 in List.map (fn v => if is_var v then T else v) t1 end;
|
H A D | commonTools.sml | 148 fun is_bool_var v = is_var v andalso (Type.compare(type_of v,bool)=EQUAL)
|
H A D | lzConv.sml | 458 if is_var arg_t then 1292 if not(is_var v) 1404 if not(is_var x)
|
H A D | lzPairRules.sml | 36 if is_var p then ABS p th 242 if is_var p then BETA_CONV tm 270 if is_var p 279 if is_var bp 282 if is_var np 344 if is_var tm then mem tm V else 374 fun new_pair p s = if is_var p then new_var p s else let val (p1,p2) = dest_pair p in mk_pair(new_pair p1 s,new_pair p2 s) end 392 in if is_var np 393 then if is_var opr then ALPHA_CONV np tm 403 if is_var op [all...] |
/seL4-l4v-10.1.1/HOL4/examples/PSL/regexp/ |
H A D | matcherScript.sml | 45 val assumer = if is_var l then K ALL_TAC else ASSUME_TAC
|
/seL4-l4v-10.1.1/HOL4/examples/acl2/examples/M1/ |
H A D | sexp.sml | 1045 if is_var tm 1114 if is_var opr 1187 if is_var tm then fst(dest_var tm) 1809 if is_var tm
|
/seL4-l4v-10.1.1/HOL4/examples/acl2/examples/acl2-hol-ltl-paper-example/ |
H A D | sexp.sml | 971 if is_var tm 1040 if is_var opr 1113 if is_var tm then fst(dest_var tm) 1735 if is_var tm
|
/seL4-l4v-10.1.1/HOL4/examples/acl2/ml/ |
H A D | acl2encodeLib.sml | 1240 val pvars = filter is_var (mapfilter (rand o rator) coders)
|
H A D | encodeLib.sml | 901 val vars = filter is_var hfuns 1733 (if is_var (rand (rhs g)) then
|
H A D | functionEncodeLib.sml | 133 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...] |
H A D | polytypicLib.sml | 509 val _ = assert "GEN_THM" [("List is not a list of variables",all is_var)] list 625 val all_vars = find_terms is_var term 1043 val _ = assert' [("Function list is not a list of variables",all is_var)] fvs
|
H A D | sexp.sml | 971 if is_var tm 1040 if is_var opr 1113 if is_var tm then fst(dest_var tm) 1735 if is_var tm
|
H A D | translateLib.sml | 35 (if is_var fx' then (subst [inst_it fx' fy' fx' |-> fy']) 37 else (if is_var fy' then (subst [inst_it fy' fx' fy' |-> fx'] o inst_it fy' fx') else raise match))) 39 | (fy,[]) => if is_var fy then subst [inst_it fy t1 fy |-> t1] o inst_it fy t1 else raise match) 41 if is_var fx then (subst [inst_it fx t2 fx |-> t2]) else 42 (if same_const fx t2 then I else (if is_var t2 then (subst [inst_it t2 fx t2 |-> fx] o inst_it t2 fx) else raise match)) 77 if is_var (var thm)
|
/seL4-l4v-10.1.1/HOL4/examples/dev/Fact32/ |
H A D | NOT32.ml | 56 andalso all is_var (strip_pair(rand tm))
|
H A D | exor32.ml | 89 andalso all is_var (strip_pair(rand tm))
|
/seL4-l4v-10.1.1/HOL4/examples/dev/ |
H A D | compile.sml | 139 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/examples/dev/sw/ |
H A D | ANF.sml | 136 else if is_var t orelse is_word_literal t orelse numSyntax.is_numeral t orelse is_const t
|
H A D | IR.sml | 189 if is_var exp then
|
/seL4-l4v-10.1.1/HOL4/examples/dev/sw/working/0.1/ |
H A D | ANF.sml | 136 else if is_var t orelse is_word_literal t orelse numSyntax.is_numeral t orelse is_const t
|
Completed in 290 milliseconds
12345678