Searched refs:mk_var (Results 1 - 25 of 368) sorted by path

1234567891011>>

/seL4-l4v-10.1.1/HOL4/Manual/Description/
H A DQuantHeuristics.tex497 val x = mk_var (v_name ^ "_hd", v_ty);
498 val xs = mk_var (v_name ^ "_tl", v_list_ty);
/seL4-l4v-10.1.1/HOL4/Manual/Translations/IT/Description/
H A DQuantHeuristics.tex487 val x = mk_var (v_name ^ "_hd", v_ty);
488 val xs = mk_var (v_name ^ "_tl", v_list_ty);
H A Dsystem.tex298 \index{mk_var@\ml{mk\_var}|pin}
300 mk_var : (string * hol_type) -> term
469 (mk_var("x",numty),
473 mk_var("x", numty)),
559 (mk_var("x",bool),
560 mk_eq(mk_var("x",numty),
779 \index{mk_var@\ml{mk\_var}}
791 {\small\verb+mk_var("+}$var${\small\verb+",+}$\sigma${\small\verb+)+} \\ \hline
/seL4-l4v-10.1.1/HOL4/Manual/Translations/IT/Tutorial/
H A Dlogic.tex118 La funzione \ml{mk_var} costruisce una variabile da una stringa e un tipo.
124 - val x = mk_var("x", ``:bool``)
125 and y = mk_var("y", ``:bool``)
126 and z = mk_var("z", ``:bool``);
/seL4-l4v-10.1.1/HOL4/Manual/Tutorial/
H A Dlogic.tex118 The function \ml{mk_var} constructs a variable from a string and a type.
124 - val x = mk_var("x", ``:bool``)
125 and y = mk_var("y", ``:bool``)
126 and z = mk_var("z", ``:bool``);
/seL4-l4v-10.1.1/HOL4/examples/ARM/arm6-verification/
H A DarmLib.sml56 val X = variant vlist (mk_var("x",type_of M))
65 val X = variant vlist (mk_var("x",type_of M))
/seL4-l4v-10.1.1/HOL4/examples/ARM/v4/
H A DarmLib.sml43 val X = variant vlist (mk_var("x",type_of M))
52 val X = variant vlist (mk_var("x",type_of M))
H A Darm_emitScript.sml54 FAIL num2register ^(mk_var("30 < n",bool)) n`,
75 FAIL num2condition ^(mk_var("15 < n",bool)) n`,
H A DinstructionSyntax.sml36 | mk_register (VReg x) = mk_var (x, ``:word4``);
/seL4-l4v-10.1.1/HOL4/examples/ARM/v7/
H A Darm_parserLib.sml408 fun cast_var ty v = mk_var (fst (dest_var v),ty);
825 next_token >>- return (mk_var (Substring.string s,ty))
1089 mk_var (s,``:word4``)
H A Darm_random_testingLib.sml633 fun reg tm = mk_var ("r" ^ Int.toString (uint_of_word tm), ``:word32``);
634 fun flag tm = mk_var (fst (dest_const tm), bool);
635 val arch = mk_var ("architecture",``:ARMarch``)
636 val cpsr = mk_var ("cpsr", ``:ARMpsr``)
637 val spsr = mk_var ("spsr", ``:ARMpsr``)
638 val GE = mk_var ("GE", ``:word4``)
639 val IT = mk_var ("IT", ``:word8``)
640 val teehbr = mk_var ("TEEHBR", ``:word32``)
641 val mode = mk_var ("mode", ``:word5``)
642 val mem = mk_var ("me
[all...]
H A Darm_stepLib.sml1154 val the_state = mk_var ("state",``:arm_seq_monad$arm_state``)
H A Dselftest.sml66 fun flag tm = mk_var (fst (dest_const tm), bool);
67 fun spsr_flag tm = mk_var ("s" ^ fst (dest_const tm), bool);
95 val GE = mk_var ("GE", ``:word4``);
96 val spsrGE = mk_var ("spsrGE", ``:word4``);
98 val mode = mk_var ("mode", ``:word5``);
99 val spsrmode = mk_var ("spsrmode", ``:word5``);
101 fun reg i = mk_var ("r" ^ Int.toString i, ``:word32``);
120 val mem = mk_var ("mem", ``:word32 -> word8``);
/seL4-l4v-10.1.1/HOL4/examples/ARM/v7/eval/
H A Darm_emitScript.sml33 FAIL bytes ^(mk_var("n not 1, 2 or 4",bool)) (w,n)`,
49 | _ => FAIL parallel_add_sub_op1 ^(mk_var("can't decode",bool)) w`,
62 | _ => FAIL parallel_add_sub_op2 ^(mk_var("can't decode",bool)) w`,
76 ^(mk_var("can't decode",bool)) w`,
H A Darm_evalLib.sml441 fun reg n = mk_var ("r" ^ Int.toString n, ``:word32``)
442 fun psr n = mk_var ("r" ^ Int.toString n, ``:ARMpsr``)
496 (mk_var ("r" ^ Int.toString i, typ) |->
H A Darm_evalScript.sml146 fun reg n = mk_var ("r" ^ Int.toString n, ``:word32``)
175 fun psr n = mk_var ("r" ^ Int.toString n, ``:ARMpsr``)
/seL4-l4v-10.1.1/HOL4/examples/ARM_security_properties/
H A DARM_proverLib.sml418 val gen_var = (mk_var("y", abs_type))
H A DARM_prover_extLib.sml262 val gen_var = (mk_var("y", abs_type))
H A Duser_lemma_primitive_operationsScript.sml468 THEN ASSUME_TAC (SPECL [``xI:bool``, ``(s2.psrs (0,CPSR)).F:bool``, ``s1:arm_state``, mk_var ("H", H_sig)] (GEN_ALL simp_ext_lem))
469 THEN ASSUME_TAC (SPECL [``xI:bool``, ``(s2.psrs (0,CPSR)).F:bool``, ``s2:arm_state``, mk_var ("H", H_sig)] (GEN_ALL simp_ext_lem))
470 THEN ASSUME_TAC (SPECL (List.concat [[``s1:arm_state``], additional_spec_list, [mk_var ("H", H_sig), ``xI:bool``, ``(s2.psrs (0,CPSR)).F:bool``]]) effect_fixed_lem)
471 THEN ASSUME_TAC (SPECL (List.concat [[``s2:arm_state``], additional_spec_list, [mk_var ("H", H_sig), ``xI:bool``, ``(s2.psrs (0,CPSR)).F:bool``]]) effect_fixed_lem)
/seL4-l4v-10.1.1/HOL4/examples/CCS/
H A DCCSConv.sml152 val U = mk_var ("u", type_of (hd actl));
302 val U = mk_var ("u", type_of (hd actl));
/seL4-l4v-10.1.1/HOL4/examples/HolBdd/
H A DDerivedBddRules.sml215 else Psyntax.mk_cond(mk_var(get_node_name(bdd.var bdd),bool),
318 val ntm = mk_var("n",num)
692 SOME(s,_) => BddVar true vm (mk_var(s,bool))
807 val prime_var = mk_var o (prime ## I) o dest_var
904 SOME(s,_) => mk_var(s,bool)
/seL4-l4v-10.1.1/HOL4/examples/HolBdd/Examples/KatiPuzzle/
H A DKatiPuzzleScript.sml76 (fn s => mk_var(s,bool))
167 (mk_var("s",type_of s))
/seL4-l4v-10.1.1/HOL4/examples/HolBdd/Examples/Solitaire/
H A DHexSolitaireScript.sml80 if n<10 then mk_var("v0"^(int_to_string n),bool)
81 else mk_var("v"^(int_to_string n),bool);
84 if n<10 then mk_var("v0"^(int_to_string n)^"'",bool)
85 else mk_var("v"^(int_to_string n)^"'",bool);
93 fun mk_bool_var s = mk_var(s,bool);
H A DMiniTLHexSolitaireScript.sml63 if n<10 then mk_var("v0"^(int_to_string n),bool)
64 else mk_var("v"^(int_to_string n),bool);
71 if n<10 then mk_var("v0"^(int_to_string n)^"'",bool)
72 else mk_var("v"^(int_to_string n)^"'",bool);
95 (fn s => mk_var(s,bool))
199 (mk_var("s",type_of s))
H A DSolitaireScript.sml71 fun mk_bool_var s = mk_var(s,bool)

Completed in 164 milliseconds

1234567891011>>