| /seL4-l4v-10.1.1/HOL4/src/quotient/examples/ |
| H A D | tactics.sml | 407 val (var,body) = dest_abs bodyf; value
420 val (var,body) = dest_abs bodyf; value
|
| /seL4-l4v-10.1.1/HOL4/examples/lambda/other-models/ |
| H A D | ncScript.sml | 355 and var = Term`\s:string. (VAR s:'a nc, (var s:'b) )` value
[all...] |
| /seL4-l4v-10.1.1/HOL4/examples/muddy/ |
| H A D | bdd.sml | 81 val var : bdd -> varnum = app1 (symb "mlbdd_bdd_var") value
192 else let val var = var bdd value
|
| /seL4-l4v-10.1.1/HOL4/examples/muddy/muddyC/buddy/src/ |
| H A D | bddop.c | 896 bdd_restrict(BDD r, BDD var) argument
1231 bdd_compose(BDD f, BDD g, int var) argument
1541 bdd_exist(BDD r, BDD var) argument
1592 bdd_forall(BDD r, BDD var) argument
1646 bdd_unique(BDD r, BDD var) argument
1745 bdd_appex(BDD l, BDD r, int opr, BDD var) argument
1811 bdd_appall(BDD l, BDD r, int opr, BDD var) argument
1877 bdd_appuni(BDD l, BDD r, int opr, BDD var) argument
2203 bdd_satoneset(BDD r, BDD var, BDD pol) argument
2229 satoneset_rec(BDD r, BDD var) argument
[all...] |
| H A D | reorder.c | 1019 static int reorder_makenode(int var, int low, int high) argument
1401 reorder_varup(int var) argument
1451 reorder_vardown(int var) argument
1974 bdd_var2level(int var) argument
[all...] |
| H A D | bdd.h | 597 inline bdd bdd_restrict(const bdd &r, const bdd &var) argument
633 inline bdd bdd_exist(const bdd &r, const bdd &var) argument
636 inline bdd bdd_forall(const bdd &r, const bdd &var) argument
639 bdd_unique(const bdd &r, const bdd &var) argument
642 bdd_appex(const bdd &l, const bdd &r, int op, const bdd &var) argument
645 bdd_appall(const bdd &l, const bdd &r, int op, const bdd &var) argument
648 bdd_appuni(const bdd &l, const bdd &r, int op, const bdd &var) argument
657 bdd_satoneset(const bdd &r, const bdd &var, const bdd &pol) argument
[all...] |
| /seL4-l4v-10.1.1/HOL4/examples/muddy/muddyC/ |
| H A D | muddy.c | 302 EXTERNML value mlbdd_bdd_restrict(value r, value var) /* ML */ argument
308 EXTERNML value mlbdd_bdd_compose(value f, value g, value var) /* ML */ argument
740 EXTERNML value mlfdd_domainsize(value var) /* ML */ argument
746 EXTERNML value mlfdd_varnum(value var) /* ML */ argument
752 EXTERNML value mlfdd_vars(value var) /* ML */ argument
774 mlfdd_ithset(value var) argument
780 mlfdd_domain(value var) argument
890 mlbvec_var(value bits, value var, value step) argument
896 mlbvec_varfdd(value var) argument
[all...] |
| /seL4-l4v-10.1.1/HOL4/examples/acl2/ml/ |
| H A D | acl2encodeLib.sml | 1416 let val var = fst (dest_var (fst (dest_abs term))) value
|
| H A D | encodeLib.sml | 1069 val var = mk_var("x",t) value
1094 val var = mk_var("x",target) value
1119 val var value
1968 val var = variant (thm_frees apped) (mk_var("x",t)); value
2211 val var = mk_var("x",t); value
[all...] |
| H A D | functionEncodeLib.sml | 547 let val (var,body) = with_exn dest_forall term err value
566 let val (var,body) = with_exn dest_forall term err value
591 let val (var,body) = with_exn dest_forall term err value
1739 let val var value
1755 then let val var = case (total (tryfind (hd o free_vars)) constructors) value
2055 let val (var,body) = dest_exists term value
2129 val var = variant nvars (mk_var("argument",initial_type)); value
2145 let val (var,body) = dest_forall term value
2226 val var = mk_var("arg",fst (dom_rng (type_of (hd lhss)))) value
2286 val var = genvar t value
2308 val var = genvar t value
2368 val var = mk_var("arg",t) value
2448 val var = mk_var("argument",t); value
3437 val var = mk_var("x",target); value
3499 val var = (rand o lhs o concl) detector value
3517 val var = mk_var("x",target); value
3612 let val (var,args) = strip_comb (mlhs func) value
3884 let val var = fst (dest_forall g) value
4051 val var = rand (rand (lhs (hd props'))) value
4071 let val var = mk_var("x",target) value
[all...] |
| H A D | polytypicLib.sml | 1004 val var = rand l handle e => raise err value
1275 let val var = rand func value
1379 val var = with_exn (rand o lhs o snd o dest_forall) body exn; value
1416 let val var = make_var (fst a) value
1688 val var = lhs right value
1701 val var = mk_var("x",target_type) value
1747 val var = rand conc value
3555 let val var = type_of (hd (fst (strip_forall (rhs (concl thm))))) value
[all...] |
| /seL4-l4v-10.1.1/isabelle/src/Tools/Metis/src/ |
| H A D | Term.sml | 15 type var = Name.name; type
663 val var = varName bv >> (Var o Name.fromString) value
|
| H A D | Tptp.sml | 136 fun var i = function
|
| /seL4-l4v-10.1.1/l4v/isabelle/src/Tools/Metis/src/ |
| H A D | Term.sml | 15 type var = Name.name; type
663 val var = varName bv >> (Var o Name.fromString) value
|
| H A D | Tptp.sml | 136 fun var i = function
|
| /seL4-l4v-10.1.1/HOL4/src/datatype/mutrec/ |
| H A D | MutRecDef.sml | 1222 let val var = variant (all_vars tm2) v value
1377 val var = mk_var{Name= "x"^(int_to_string num), value
[all...] |
| /seL4-l4v-10.1.1/HOL4/src/integer/ |
| H A D | CooperCore.sml | 816 val (var, rem) = (I ## SOME) (dest_plus r) value
984 val (var, rem) = (I ## SOME) (dest_plus r) value
1174 val (var, body) = dest_exists tm value
|
| H A D | CooperMath.sml | 569 val (var, rest) = Lib.pluck is_var mcands value
889 val (var, body) = Psyntax.dest_exists term value
963 val (var, body) = dest_exists tm value
[all...] |
| /seL4-l4v-10.1.1/HOL4/examples/machine-code/graph/ |
| H A D | derive_specsLib.sml | 239 val var = ``var:bool`` value
|
| /seL4-l4v-10.1.1/HOL4/polyml/mlsource/MLCompiler/ParseTree/ |
| H A D | TYPECHECK_PARSETREE.sml | 538 val var = mkVar(name, mkTypeVar (level, false, false, false), props) value
[all...] |
| /seL4-l4v-10.1.1/HOL4/polyml/mlsource/MLCompiler/ |
| H A D | TYPEIDCODE.sml | 1214 val var = vaLocal(idAccess(tcIdentifier(tsConstr typeConstr))) value
|
| /seL4-l4v-10.1.1/HOL4/src/1/ |
| H A D | ConseqConv.sml | 416 val (var, body) = dest_forall t; value
429 val (var, body) = dest_exists t; value
|
| H A D | Conv.sml | 2482 val (var, body) = dest_exists t value
|
| H A D | Drule.sml | 32 val (var, cmb) = dest_abs t value
|
| /seL4-l4v-10.1.1/HOL4/src/bool/ |
| H A D | boolScript.sml | 344 let val (var, cmb) = dest_abs t value
|