Searched refs:Type (Results 151 - 175 of 497) sorted by relevance

1234567891011>>

/seL4-l4v-10.1.1/HOL4/src/HolSmt/
H A DYices.sml180 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 DmungeTools.sml6 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 Dholindex-demo.tex109 @Type{type_id_4,
267 \renewcommand[\protect]{\citeHOLty}[1]{(HOL-Type~\citePureHOLty{#1})}
282 \renewenvironment{HOLTypeIndex}{\section*{HOL-Type Index}}{}
H A Dmunger.lex109 Type, optstring, args);
/seL4-l4v-10.1.1/HOL4/examples/dev/sw/
H A DpreARMScript.sml25 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 DpreARMScript.sml22 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 DPreterm.sml11 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 DParseDatatype.sml32 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 DFCNet.sml337 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 DTerm.sml4 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 Dm0_progLib.sml10 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 DRecordType.sml20 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 DpreARMScript.sml21 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 DswsepLib.sml152 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 DpairSyntax.sml18 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 DnumLib.sml133 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 DtestTypesScript.sml6 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 DBmark.sml77 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 DRoundOpScript.sml44 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 Dcheri_stepLib.sml29 (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 Dx64_decompLib.sml11 val (Type, Term) = parse_from_grammars x64_progTheory.x64_prog_grammars value
/seL4-l4v-10.1.1/HOL4/polyml/modules/IntInfAsInt/
H A DROOT.sml83 val typeVals = map (dolookup(#lookupType, Tags.typeTag, "Type"))
/seL4-l4v-10.1.1/HOL4/src/finite_map/
H A Dfinite_mapSyntax.sml28 else raise ERR "dest_fmap_ty" "Type not a finite map"
/seL4-l4v-10.1.1/HOL4/src/floating-point/
H A Dfp-functor.sml3 val ty: Type.hol_type) :> fpSyntax =
/seL4-l4v-10.1.1/HOL4/src/new-datatype/
H A DNDatatype.sml15 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.")

Completed in 307 milliseconds

1234567891011>>