Searched refs:Type (Results 126 - 150 of 497) sorted by relevance

1234567891011>>

/seL4-l4v-10.1.1/HOL4/src/datatype/mutrec/examples/
H A Dexample.sml20 val var_ty = Parse.Type`:var`;
146 quotations that define mutually recursive functions. Type inference will
/seL4-l4v-10.1.1/HOL4/src/metis/
H A DfolTools.sml14 val (Type,Term) = parse_from_grammars normalFormsTheory.normalForms_grammars value
583 fun h v = Term.mk_var (v, Type.alpha);
588 val a' = map (g Type.alpha) a
589 val ty = Lib.funpow (length a) (fn x => Type.--> (Type.alpha,x)) ty
597 | f (Atom (Fn ("=",[x,y]))) = mk_eq (g Type.alpha x, g Type.alpha y)
598 | f (Atom tm) = g Type.bool tm
H A DfolTools.sig15 type hol_type = Type.hol_type
/seL4-l4v-10.1.1/HOL4/src/num/arith/src/
H A DThm_convs.sml171 REWR_CONV (INST_TYPE [alpha |-> Type`:num`] COND_RATOR);
174 REWR_CONV (INST_TYPE [alpha |-> Type`:num`] COND_RAND);
/seL4-l4v-10.1.1/HOL4/src/string/
H A DstringSyntax.sml14 val char_ty = Type.mk_thy_type {Tyop = "char", Thy = "string", Args = []}
15 val string_ty = Type.mk_thy_type {Tyop = "list", Thy = "list", Args = [char_ty]}
/seL4-l4v-10.1.1/HOL4/examples/dev/AES/tupled/
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/dev/AES/word8/
H A DRoundOpScript.sml42 Type`:word8 # word8 # word8 # word8 #
47 val _ = type_abbrev("state", Type`:block`);
48 val _ = type_abbrev("key", Type`:state`);
49 val _ = type_abbrev("w8x4", Type`:word8 # word8 # word8 # word8`);
/seL4-l4v-10.1.1/HOL4/src/0/
H A DSubst.sml10 (* Type of explicit substitutions on an abstract type of term 'a. *)
/seL4-l4v-10.1.1/HOL4/src/1/
H A DRsyntax.sig3 type hol_type = Type.hol_type
H A DTypeBasePure.sml15 let val {Thy,Tyop,Args} = Type.dest_thy_type ty
624 val (inst0, _) = recurse (Binarymap.mkDict Type.compare, Type.alpha) [ty]
629 Type.type_subst inst ty
633 case Type.op_arity {Thy = thy, Tyop = tyop} of
670 if Type.is_vartype ty then 1
672 val {Args,...} = Type.dest_thy_type ty
678 val (i, sames) = Type.raw_match_type pat ty ([], [])
834 if ty = Type.bool then bool_var
1048 field "ty" (Type (#t
[all...]
/seL4-l4v-10.1.1/HOL4/src/HolQbf/
H A Dselftest.sml83 fun f n = Term.mk_var("v"^(Int.toString n),Type.bool)
/seL4-l4v-10.1.1/HOL4/src/enumfset/
H A DtotoTacs.sml71 val var1 = mk_var ("_z", Type`:bool`); (* supposedly not an identifier *)
122 in if is_const ans andalso type_of ans = Type`:cpn` then eqn else
164 in if is_const ans andalso type_of ans = Type`:cpn` then eqn else
210 (* ******* Type string treated as synonymous with char list ******* *)
/seL4-l4v-10.1.1/HOL4/src/lite/
H A DliteLib.sml241 let val ty = Lib.fst(Type.dom_rng(Term.type_of tm1))
242 val tyins = Type.match_type ty (Term.type_of tm2)
444 let val theta = [{redex=Type.alpha, residue=Term.type_of v}]
448 let val theta = [{redex=Type.alpha, residue=Term.type_of v}]
/seL4-l4v-10.1.1/HOL4/src/marker/
H A DmarkerSyntax.sml92 Type.compare(type_of l, label_ty) = EQUAL orelse
/seL4-l4v-10.1.1/HOL4/src/parse/
H A DTermParse.sig5 type hol_type = Type.hol_type
H A DHol_pp.sml46 vblock ("Type constants",
139 add_string "Type" >> add_break (1,0) >>
152 add_string "Type"
H A DLiteral.sml36 if Type.is_vartype ty then false
37 else case Type.dest_thy_type ty
42 let val (ty1,ty2) = Type.dom_rng ty
/seL4-l4v-10.1.1/HOL4/src/postkernel/
H A DSharingTables.sml4 open Term Type
117 {tysize = 0, tymap = Map.mkDict Type.compare, tylist = [] }
122 TYV s => (n + 1, Map.insert(tymap, n, Type.mk_vartype s))
130 Type.mk_thy_type {Thy = Thy, Tyop = Other,
/seL4-l4v-10.1.1/HOL4/src/sort/
H A DternaryComparisonsScript.sml13 (INST_TYPE[Type.alpha |-> ``:ordering``] REFL_CLAUSE
/seL4-l4v-10.1.1/HOL4/src/tfl/src/
H A Dselftest.sml21 test "Type-constrainted constant as parameter"
/seL4-l4v-10.1.1/HOL4/examples/pgcl/src/
H A DrelScript.sml76 val () = type_abbrev ("rel", Type `:'a state -> 'a state measure -> bool`);
/seL4-l4v-10.1.1/HOL4/examples/Crypto/AES/
H A DRoundOpScript.sml42 Type`:word8 # word8 # word8 # word8 #
47 val _ = type_abbrev("state", Type`:block`);
48 val _ = type_abbrev("key", Type`:state`);
49 val _ = type_abbrev("w8x4", Type`:word8 # word8 # word8 # word8`);
/seL4-l4v-10.1.1/isabelle/src/HOL/Bali/document/
H A Droot.tex108 \item[Type]
199 \chapter{Type}
200 \input{Type}
/seL4-l4v-10.1.1/l4v/isabelle/src/HOL/Bali/document/
H A Droot.tex108 \item[Type]
199 \chapter{Type}
200 \input{Type}
/seL4-l4v-10.1.1/HOL4/examples/muddy/
H A Dbdd.sig150 Type [bdd] is the abstract type of BDDs.
197 Type [varSet] is an effective representation of sets of variables.
224 Type [bddop] represent the binary boolean operator which can be used
278 Type [pairSet] is used to represet substitutions of variables with
288 Type [assignment] represents an assignment of variables. The

Completed in 274 milliseconds

1234567891011>>