/seL4-l4v-10.1.1/HOL4/src/datatype/mutrec/examples/ |
H A D | example.sml | 20 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 D | folTools.sml | 14 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 D | folTools.sig | 15 type hol_type = Type.hol_type
|
/seL4-l4v-10.1.1/HOL4/src/num/arith/src/ |
H A D | Thm_convs.sml | 171 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 D | stringSyntax.sml | 14 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 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/dev/AES/word8/ |
H A D | RoundOpScript.sml | 42 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 D | Subst.sml | 10 (* Type of explicit substitutions on an abstract type of term 'a. *)
|
/seL4-l4v-10.1.1/HOL4/src/1/ |
H A D | Rsyntax.sig | 3 type hol_type = Type.hol_type
|
H A D | TypeBasePure.sml | 15 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 D | selftest.sml | 83 fun f n = Term.mk_var("v"^(Int.toString n),Type.bool)
|
/seL4-l4v-10.1.1/HOL4/src/enumfset/ |
H A D | totoTacs.sml | 71 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 D | liteLib.sml | 241 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 D | markerSyntax.sml | 92 Type.compare(type_of l, label_ty) = EQUAL orelse
|
/seL4-l4v-10.1.1/HOL4/src/parse/ |
H A D | TermParse.sig | 5 type hol_type = Type.hol_type
|
H A D | Hol_pp.sml | 46 vblock ("Type constants", 139 add_string "Type" >> add_break (1,0) >> 152 add_string "Type"
|
H A D | Literal.sml | 36 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 D | SharingTables.sml | 4 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 D | ternaryComparisonsScript.sml | 13 (INST_TYPE[Type.alpha |-> ``:ordering``] REFL_CLAUSE
|
/seL4-l4v-10.1.1/HOL4/src/tfl/src/ |
H A D | selftest.sml | 21 test "Type-constrainted constant as parameter"
|
/seL4-l4v-10.1.1/HOL4/examples/pgcl/src/ |
H A D | relScript.sml | 76 val () = type_abbrev ("rel", Type `:'a state -> 'a state measure -> bool`);
|
/seL4-l4v-10.1.1/HOL4/examples/Crypto/AES/ |
H A D | RoundOpScript.sml | 42 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 D | root.tex | 108 \item[Type] 199 \chapter{Type} 200 \input{Type}
|
/seL4-l4v-10.1.1/l4v/isabelle/src/HOL/Bali/document/ |
H A D | root.tex | 108 \item[Type] 199 \chapter{Type} 200 \input{Type}
|
/seL4-l4v-10.1.1/HOL4/examples/muddy/ |
H A D | bdd.sig | 150 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
|