Searched refs:Type (Results 201 - 225 of 497) sorted by relevance

1234567891011>>

/seL4-l4v-10.1.1/HOL4/src/postkernel/
H A DHolKernel.sml4 open Feedback Globals Lib Type Term Thm Theory
210 val mk_aty = list_mk_rbinop (Lib.curry Type.-->)
219 Term.list_mk_comb (Term.inst (Type.match_type tyl tyr) tm, xs)
504 val name = fst (dest_var (genvar Type.alpha))
620 if existing = residue then E else failwith "Type bindings clash"
H A DTheoryPP.sml12 type hol_type = Type.hol_type
48 let open Portable Type PP
274 add_string "open Type Term Thm" >> add_newline >>
H A DTheory.sig4 type hol_type = Type.hol_type
/seL4-l4v-10.1.1/HOL4/src/quotient/src/
H A Dquotient.sig49 val list_cache : unit -> (Type.hol_type * Thm.thm) list
102 Type.hol_type -> (* type, whose equivalence relation is equality *)
141 Type.hol_type -> (* type, whose equivalence relation is desired *)
157 Type.hol_type -> (* type, whose equivalence relation is equality *)
210 Type.hol_type -> (* type (not lifted) of desired quotient *)
/seL4-l4v-10.1.1/HOL4/examples/separationLogic/src/
H A Dvars_as_resourceBaseFunctor.sml829 val base_t0 = inst [Type.alpha |-> var_ty,
830 Type.beta |-> data_ty,
831 Type.gamma |-> (optionSyntax.mk_option data_ty)] var_res_exp_varlist_update_term;
833 val var_exp_t = inst [Type.beta |-> var_ty, Type.alpha |-> data_ty]
/seL4-l4v-10.1.1/HOL4/examples/separationLogic/src/holfoot/
H A DholfootParser.sml150 val eL_v = genvar (Type `:num list`);
423 (map string2holfoot_tag argL), Type `:holfoot_tag`);
620 val rp_term = pred_setSyntax.prim_mk_set (rL, Type `:holfoot_var`);
621 val wp_term = pred_setSyntax.prim_mk_set (wL, Type `:holfoot_var`);
649 val rp_term = listSyntax.mk_list (var_list, Type `:holfoot_var`);
694 val unit_var_term = mk_var("uv", Type `:unit`);
1110 val arg_ref_term = mk_new_var ("arg_refL", Type `:holfoot_var list`);
1111 val arg_val_term = mk_new_var ("arg_valL", Type `:num list`);
1309 val varL = listSyntax.mk_list (vars, Type `:holfoot_var`);
1314 Type `
[all...]
/seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/common/
H A DstateLib.sml11 val (Type, Term) = value
94 val ty_name = #Tyop o Type.dest_thy_type o Term.type_of
107 val state_ty = fst (Type.dom_rng ty)
108 val {Thy = thy, ...} = Type.dest_thy_type state_ty
119 (combinSyntax.mk_K_1 (c, Type.alpha), Type.alpha, true)
247 (pairSyntax.mk_prod (Type.dom_rng ty) --> Type.bool) --> Type.bool
326 case Type
[all...]
/seL4-l4v-10.1.1/HOL4/examples/ARM_security_properties/
H A Duser_lemma_instructionsScript.sml439 val _ = e(ASSUME_TAC (SPECL [``n:word4``, load_multiple_part, ``(assert_mode 16w)``, ``priv_mode_constraints``, ``priv_mode_similar``] (INST_TYPE [alpha |-> Type `:unit`] cpsr_par_simp_rel_lem)));
585 val data_processing_core_part_thm2 = SIMP_RULE (srw_ss()) [(SPECL [data_processing_core_part, ``(assert_mode 16w):(arm_state->bool)``, ``(assert_mode 16w):(arm_state->bool)``] (INST_TYPE [alpha |-> (Type `:(word32 # (word32 # bool) # bool # bool #bool # bool)`), beta |-> type_of (``()``)] second_abs_lemma))] data_processing_core_part_thm1;
595 val _ = e(ASSUME_TAC (SPECL [data_processing_pre_part, data_processing_core_part,``16w:word5``, ``priv_mode_constraints``, ``priv_mode_similar``] (INST_TYPE [alpha |-> Type `:(word32 # (word32 # bool) # bool # bool #bool # bool)`, beta |-> type_of (``()``)] seqT_preserves_relation_uu_thm)));
763 THEN ASSUME_TAC (SPEC ``(��info. if version_number info.arch < 5 then take_undef_instr_exception <|proc := 0|> else take_prefetch_abort_exception <|proc := 0|>)`` (INST_TYPE [alpha |-> Type `:ARMinfo`, beta |-> Type `:unit`] second_abs_lemma))
765 THEN ASSUME_TAC (SPECL [``(read_info <|proc:=0|>):(ARMinfo M)``, ``( \info. (if version_number info.arch < 5 then take_undef_instr_exception <|proc := 0|> else take_prefetch_abort_exception <|proc := 0|>))``, ``16w:word5``, ``little_mode_mix``, ``little_mode_mix``, ``priv_mode_constraints_v1``, ``priv_mode_similar``] (INST_TYPE [alpha |-> Type `:ARMinfo`, beta |-> Type `:unit`] seqT_preserves_relation_comb_thm))
/seL4-l4v-10.1.1/HOL4/examples/dev/sw/
H A DIRSyntax.sml240 mk_list (List.map (term_of_int o index_of_exp) slist, Type `:num`)]),
244 mk_list (List.map (term_of_int o index_of_exp) dlist, Type `:num`)]), 0)
267 val blk = mk_comb (Term`BLK`, mk_list (l1, Type`:DOPER`));
/seL4-l4v-10.1.1/HOL4/src/HolSat/
H A DdimacsTools.sml6 open Lib boolLib Globals Parse Term Type Thm Drule Conv Feedback
176 then mk_var(((!prefix) ^ Int.toString n), Type.bool)
177 else mk_neg(mk_var(((!prefix) ^ Int.toString(Int.abs n)), Type.bool));
H A DsatTools.sml10 open Lib boolLib Globals Parse Term Type Thm Drule Psyntax Conv Feedback
/seL4-l4v-10.1.1/HOL4/src/TeX/
H A Dholindex.sml186 | command2string mungeTools.Type = "Type";
255 List.map (output_holtex_def mungeTools.Type "\\defineHOLty{" os)
/seL4-l4v-10.1.1/HOL4/src/holyhammer/
H A DhhWriter.sml177 val less_ty = fn a => (fn b => Type.compare (a,b) = LESS)
389 tyvar_names = ref (dempty Type.compare),
437 tyvar_names = ref (dempty Type.compare),
H A DhhTptp.sml103 (* Type unsafe version *)
/seL4-l4v-10.1.1/HOL4/examples/HolCheck/
H A DctlScript.sml374 val _ = overload_on ("~", mk_const("~",Type`:bool -> bool`));
377 val _ = overload_on ("~", mk_const("~",Type`:bool -> bool`));
378 fun prepOverload s = overload_on (s, mk_const(s,Type`:bool -> bool -> bool`));
/seL4-l4v-10.1.1/seL4/manual/parts/
H A Dbootup.tex92 Field Type & Field Name & Description \\
131 Field Type & Field Name & Description \\
182 Field Type & Field Name & Description \\
/seL4-l4v-10.1.1/HOL4/examples/dev/AES/tupled/
H A Dword8Script.sml14 val _ = type_abbrev("word8", Type`:bool#bool#bool#bool#bool#bool#bool#bool`);
/seL4-l4v-10.1.1/HOL4/examples/dev/sw/working/0.2/
H A DCFLScript.sml48 val _ = type_abbrev("MMEM", Type`:num # OFFSET`); (* memory in ir *)
167 val _ = type_abbrev("CEXP", Type`:MREG # COND # MEXP`);
404 (INST_TYPE [alpha |-> Type `:word32 # (num |-> word32) # (num |-> word32)`] UPLOAD_LEM_2)),
408 (INST_TYPE [alpha |-> Type `:word32 # (num |-> word32) # (num |-> word32)`] UPLOAD_LEM_2)),
/seL4-l4v-10.1.1/HOL4/src/0/
H A DNet.sig37 is supplied when the item is inserted into the net. Type information,
/seL4-l4v-10.1.1/HOL4/src/1/
H A DTypeBasePure.sig3 type hol_type = Type.hol_type
/seL4-l4v-10.1.1/HOL4/src/Boolify/test/
H A Dtest.sml100 MATCH_MP (INST_TYPE [alpha |-> Type`:num`] decode_list)
/seL4-l4v-10.1.1/HOL4/src/experimental-kernel/
H A DNet.sig37 is supplied when the item is inserted into the net. Type information,
/seL4-l4v-10.1.1/HOL4/src/num/arith/src/
H A DnumSimps.sml21 val (Type,Term) = parse_from_grammars arithmeticTheory.arithmetic_grammars value
290 orelse (is_eq tm andalso type_of (rhs tm) = Type.bool) then
338 (type_of tm = Type.bool) andalso
452 (ty=Type.bool andalso (is_arith tm orelse tm = F))
/seL4-l4v-10.1.1/HOL4/src/opentheory/postbool/
H A DOpentheory.sig2 type term = Term.term type hol_type = Type.hol_type type thm = Thm.thm
/seL4-l4v-10.1.1/HOL4/src/patricia/
H A DpatriciaSyntax.sml11 Type.mk_thy_type{Tyop="ptree", Thy="patricia", Args = [pty]};

Completed in 355 milliseconds

1234567891011>>