/seL4-l4v-10.1.1/HOL4/src/HolSmt/ |
H A D | Yices.sml | 180 if !Library.trace > 0 andalso Type.is_type ty then 245 else if Type.is_type ty then 247 let val {Thy, Tyop, Args} = Type.dest_thy_type ty 611 val (record_ty, rng_ty) = Type.dom_rng select_ty 612 val (record_name, _) = Type.dest_type record_ty 620 Lib.can (Type.match_type field_ty) rng_ty) 646 val (record_name, _) = Type.dest_type record_ty 655 Lib.can (Type.match_type field_ty) val_ty) 726 if (Lib.can Type.dom_rng) T then 728 let val v = Term.mk_var ("x", Lib.fst (Type [all...] |
/seL4-l4v-10.1.1/HOL4/src/TeX/ |
H A D | mungeTools.sml | 6 datatype command = Theorem | Term | Type 260 ((Parse.Type [QUOTE nm2] |-> Parse.Type [QUOTE nm1]) :: tyacc, instacc) 261 else (warn (loc, "Type substitution mal-formed"); die "") 263 (warn (loc, "Type substitution mal-formed"); die "") 520 | Type => let 525 else Parse.Type [QQ parse_start, QQ spec]
|
H A D | holindex-demo.tex | 109 @Type{type_id_4, 267 \renewcommand[\protect]{\citeHOLty}[1]{(HOL-Type~\citePureHOLty{#1})} 282 \renewenvironment{HOLTypeIndex}{\section*{HOL-Type Index}}{}
|
H A D | munger.lex | 109 Type, optstring, args);
|
/seL4-l4v-10.1.1/HOL4/examples/dev/sw/ |
H A D | preARMScript.sml | 25 val _ = type_abbrev("REGISTER", Type`:word4`); 35 val _ = type_abbrev("CPSR", Type`:word32`); 116 val _ = type_abbrev("ADDR", Type`:word30`); 117 val _ = type_abbrev("DATA", Type`:word32`); 118 val _ = type_abbrev("DISTANCE", Type`:num`); 154 val _ = type_abbrev("OPERATION", Type`:OPERATOR # (COND option) # bool`); 155 val _ = type_abbrev("INST", Type`:OPERATION # (EXP option) # (EXP list) # (OFFSET option)`); 161 val _ = type_abbrev("STATE", Type`: num # CPSR # (REGISTER |-> DATA) # (ADDR |-> DATA)`); 819 val _ = type_abbrev("STATEPCS", Type`:STATE # (num->bool)`); 888 `step instB`] (INST_TYPE [alpha |-> Type` [all...] |
/seL4-l4v-10.1.1/HOL4/examples/dev/sw/working/0.1/ |
H A D | preARMScript.sml | 22 val _ = type_abbrev("REGISTER", Type`:word4`); 32 val _ = type_abbrev("CPSR", Type`:word32`); 113 val _ = type_abbrev("ADDR", Type`:word30`); 114 val _ = type_abbrev("DATA", Type`:word32`); 115 val _ = type_abbrev("DISTANCE", Type`:num`); 150 val _ = type_abbrev("OPERATION", Type`:OPERATOR # (COND option) # bool`); 151 val _ = type_abbrev("INST", Type`:OPERATION # (EXP option) # (EXP list) # (OFFSET option)`); 157 val _ = type_abbrev("STATE", Type`: num # CPSR # (REGISTER |-> DATA) # (ADDR |-> DATA)`); 818 val _ = type_abbrev("STATEPCS", Type`:STATE # (num->bool)`); 887 `step instB`] (INST_TYPE [alpha |-> Type` [all...] |
/seL4-l4v-10.1.1/HOL4/src/parse/ |
H A D | Preterm.sml | 11 type hol_type = Type.hol_type 259 return (map Type.dest_vartype (Term.type_vars_in_term Tm)) 416 val avds = map Type.dest_vartype (tmlist_tyvs (free_vars t)) 438 val avds = map Type.dest_vartype (tmlist_tyvs (free_vars t)) 481 val avds = map Type.dest_vartype (tmlist_tyvs (free_vars t)) 568 * Type inference for HOL terms. Looks ugly because of error messages, but is 723 Ty = Type.bool --> Type.bool --> Type.bool} 733 val c = mk_thy_const{Name = "=", Thy = "min", Ty = ty --> ty --> Type [all...] |
H A D | ParseDatatype.sml | 32 dVartype s => Type.mk_vartype s 36 NONE => Type.mk_type(s, map pretypeToType Args) 37 | SOME t => Type.mk_thy_type{Tyop = s, Thy = t,
|
H A D | FCNet.sml | 337 Type.raw_match_type ty (type_of t2) tyS) 349 else RM rest (tminfo, Type.raw_match_type ty1 ty2 tyS) 356 RM rest (tminfo, Type.raw_match_type Ty vty tyS) 363 val tyS' = Type.raw_match_type (type_of x1) (type_of x2) tyS
|
/seL4-l4v-10.1.1/HOL4/src/experimental-kernel/ |
H A D | Term.sml | 4 open Feedback Lib KernelTypes Type 174 let val (ty1,ty2) = with_exn Type.dom_rng typ err 257 EQUAL => Type.compare(ty1, ty2) 347 EQUAL => Type.compare(ty1, ty2) 362 case Type.compare(type_of v1, type_of v2) of 430 Var(_, ty) => k (Type.type_vars ty) 431 | Const(_, ty) => k (Type.type_vars ty) 784 else case total (fst o Type.dom_rng o fst o Type.dom_rng o type_of) c of 787 let val dom = fst(Type [all...] |
/seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/m0/prog/ |
H A D | m0_progLib.sml | 10 val (Type, Term) = parse_from_grammars m0_progTheory.m0_prog_grammars value 89 (List.concat (List.map dest_opc l), Type.bool), ty) 267 val R_name_b_tm = Term.mk_comb (R_name_tm, Term.mk_var ("b", Type.bool)) 430 fun mk_bool_list l = listSyntax.mk_list (l, Type.bool) 555 fun x n = Term.mk_var ("x" ^ Int.toString n, Type.bool) 712 (listSyntax.mk_list (d_list l @ d_list r, Type.bool))
|
/seL4-l4v-10.1.1/HOL4/src/datatype/record/ |
H A D | RecordType.sml | 20 val (Type,Term) = parse_from_grammars boolTheory.bool_grammars value 171 "Type to be record has more than one constructor" 182 val tymap = Binarymap.mkDict Type.compare : (hol_type,int) Binarymap.dict 188 val tyvs = HOLset.fromList Type.compare (Type.type_vars ty) 203 val avoids = Type.type_varsl types
|
/seL4-l4v-10.1.1/HOL4/examples/dev/sw/working/0.2/ |
H A D | preARMScript.sml | 21 val _ = type_abbrev("REGISTER", Type`:num`); 31 val _ = type_abbrev("CPSR", Type`:word32`); 112 val _ = type_abbrev("ADDR", Type`:num`); 113 val _ = type_abbrev("DATA", Type`:word32`); 114 val _ = type_abbrev("DISTANCE", Type`:num`); 148 val _ = type_abbrev("OPERATION", Type`:OPERATOR # (COND option) # bool`); 149 val _ = type_abbrev("INST", Type`:OPERATION # (EXP option) # (EXP list) # (OFFSET option)`); 155 val _ = type_abbrev("STATE", Type`: ADDR # CPSR # (REGISTER |-> DATA) # (ADDR |-> DATA)`); 810 val _ = type_abbrev("STATEPCS", Type`:STATE # (num->bool)`); 879 `step instB`] (INST_TYPE [alpha |-> Type` [all...] |
/seL4-l4v-10.1.1/HOL4/examples/elliptic/swsep/ |
H A D | swsepLib.sml | 152 val input_regs = listSyntax.mk_list (map IRSyntax.convert_reg (IRSyntax.pair2list (#1 (#3 comp))), Type `:MREG`); 196 val x = mk_var ("x", Type `:word4`); 234 val fe_var = mk_var ("fe", Type `:word4 -> word32`);
|
/seL4-l4v-10.1.1/HOL4/src/coretypes/ |
H A D | pairSyntax.sml | 18 Type.mk_thy_type {Tyop = "prod", Thy = "pair", Args = [ty1, ty2]} 157 (Term.inst [Type.alpha |-> aty, Type.beta |-> bty] swap_tm, t)
|
/seL4-l4v-10.1.1/HOL4/src/num/ |
H A D | numLib.sml | 133 local val v1 = genvar Type.bool 134 and v2 = genvar Type.bool 203 val ind_thm1 = INST_TYPE [Type.alpha |-> st_type] ind_thm0
|
/seL4-l4v-10.1.1/HOL4/examples/acl2/ml/ |
H A D | testTypesScript.sml | 6 let val _ = (Parse.Type t ; ()) handle _ => Hol_datatype def 8 (types := Parse.Type t :: (!types)) 11 fun AddType t = (types := Parse.Type t :: (!types));
|
/seL4-l4v-10.1.1/HOL4/examples/bmark/ |
H A D | Bmark.sml | 77 local val FUN_EQ_LEMMA' = INST_TYPE[alpha |-> Type`:num`] FUN_EQ_LEMMA 353 val EQ_SYM_EQ' = INST_TYPE[alpha |-> Type`:num`] EQ_SYM_EQ; 569 INST_TYPE[alpha |-> Type`:num#num`, beta |-> Type`:num#num#bool`] NEXT_THM;
|
/seL4-l4v-10.1.1/HOL4/examples/dev/AES/curried/ |
H A D | RoundOpScript.sml | 44 Type`:word8 # word8 # word8 # word8 # 49 val _ = type_abbrev("state", Type`:block`); 50 val _ = type_abbrev("key", Type`:state`); 51 val _ = type_abbrev("w8x4", Type`:word8 # word8 # word8 # word8`);
|
/seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/cheri/step/ |
H A D | cheri_stepLib.sml | 29 (listSyntax.mk_list (b1 @ b2 @ b3 @ b4, Type.bool), ty32) 36 General.ignore (ty = Type.bool andalso List.length l <= 32 orelse 219 fun padded_opcode v = listSyntax.mk_list (pad_opcode v, Type.bool) 247 fun x i = Term.mk_var ("x" ^ Int.toString i, Type.bool)
|
/seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/x64/decompiler/ |
H A D | x64_decompLib.sml | 11 val (Type, Term) = parse_from_grammars x64_progTheory.x64_prog_grammars value
|
/seL4-l4v-10.1.1/HOL4/polyml/modules/IntInfAsInt/ |
H A D | ROOT.sml | 83 val typeVals = map (dolookup(#lookupType, Tags.typeTag, "Type"))
|
/seL4-l4v-10.1.1/HOL4/src/finite_map/ |
H A D | finite_mapSyntax.sml | 28 else raise ERR "dest_fmap_ty" "Type not a finite map"
|
/seL4-l4v-10.1.1/HOL4/src/floating-point/ |
H A D | fp-functor.sml | 3 val ty: Type.hol_type) :> fpSyntax =
|
/seL4-l4v-10.1.1/HOL4/src/new-datatype/ |
H A D | NDatatype.sml | 15 fun gen_tyvar _ = Type.gen_tyvar (); 95 val mk_aty = list_mk_rbinop (Lib.curry Type.-->) 104 LIST_MK_COMB (INST_TYPE (Type.match_type tyl tyr) fth) aths 170 ("Type '"^Tyop^"' not supported.")
|