/seL4-l4v-10.1.1/HOL4/examples/ARM_security_properties/ |
H A D | ARM_prover_extLib.sig | 13 val get_monad_type : Type.hol_type -> Type.hol_type 20 val get_type_inst : Type.hol_type * bool -> Type.hol_type
|
/seL4-l4v-10.1.1/HOL4/src/postkernel/ |
H A D | ThyDataSexp.sml | 13 | Type of Type.hol_type 35 | Type ty => typ ty 53 | Type ty => Type.uptodate_type ty 78 | (Type ty1, Type ty2) => Type.compare(ty1, ty2) 79 | (Type _, _) => LESS 80 | (_, Type [all...] |
/seL4-l4v-10.1.1/HOL4/src/1/ |
H A D | Psyntax.sml | 6 val mk_type = Type.mk_type 7 val dest_type = Type.dest_type
|
H A D | Abbrev.sml | 5 type hol_type = Type.hol_type
|
/seL4-l4v-10.1.1/HOL4/src/parse/ |
H A D | parse_type.sig | 22 val ty_antiq : Type.hol_type -> term 23 val dest_ty_antiq : term -> Type.hol_type
|
H A D | TypeNet.sig | 6 type hol_type = Type.hol_type
|
H A D | ParseDatatype.sig | 10 val pretypeToType : pretype -> Type.hol_type 12 val parse : type_grammar.grammar -> Type.hol_type Portable.quotation -> 30 val hparse : type_grammar.grammar -> Type.hol_type Portable.quotation ->
|
/seL4-l4v-10.1.1/isabelle/src/Pure/ |
H A D | term.scala | 20 case class Type(name: String, args: List[Typ] = Nil) extends Typ 23 val dummyT = Type("dummy") 58 case Type(name, args) => store(Type(cache_string(name), args.map(cache_typ(_))))
|
/seL4-l4v-10.1.1/l4v/isabelle/src/Pure/ |
H A D | term.scala | 20 case class Type(name: String, args: List[Typ] = Nil) extends Typ 23 val dummyT = Type("dummy") 58 case Type(name, args) => store(Type(cache_string(name), args.map(cache_typ(_))))
|
/seL4-l4v-10.1.1/HOL4/src/1/theory_tests/ |
H A D | gh168bScript.sml | 16 val ty = Parse.Type [QUOTE s]
|
/seL4-l4v-10.1.1/HOL4/src/TeX/ |
H A D | mungeTools.sig | 4 datatype command = Theorem | Term | Type
|
/seL4-l4v-10.1.1/HOL4/src/opentheory/ |
H A D | OpenTheoryCommon.sig | 12 | OType of Type.hol_type
|
/seL4-l4v-10.1.1/HOL4/src/n-bit/ |
H A D | fcpSyntax.sml | 28 Type.mk_type("bit0", [mk_numeric_type (div2 n)]) 31 Type.mk_type("one", []) 33 Type.mk_type("bit1", [mk_numeric_type (div2 (less1 n))]) 39 case Type.dest_type typ of 55 Type.mk_thy_type {Tyop = "cart", Thy = "fcp", Args = [a,b]}; 58 case Lib.total Type.dest_thy_type ty 90 let val a = snd (Type.dom_rng (Term.type_of x)) in 92 (Term.inst[Type.alpha |-> a, Type.beta |-> ty] fcp_tm, x) 98 (Term.inst[Type [all...] |
/seL4-l4v-10.1.1/HOL4/examples/machine-code/graph/ |
H A D | backgroundLib.sig | 32 val dest_sum_type : Type.hol_type -> Type.hol_type * Type.hol_type
|
/seL4-l4v-10.1.1/HOL4/examples/muddy/ |
H A D | fdd.sig | 21 Type [precision] is used to express the number of bits in an fdd. 23 Type [domain] is used to express a domain size. A value n 26 Type [fddvar] is the type of fdd variables. An fdd variable
|
/seL4-l4v-10.1.1/seL4/libsel4/tools/ |
H A D | syscall_stub_gen.py | 95 class Type(object): class in inherits:object 136 Return a new Type class representing a pointer to this 160 class PointerType(Type): 165 Type.__init__(self, base_type.name, wordsize, wordsize) 178 class CapType(Type): 183 Type.__init__(self, name, wordsize, wordsize) 185 class StructType(Type): 190 Type.__init__(self, name, size_bits, wordsize) 199 class BitFieldType(Type): 204 Type [all...] |
/seL4-l4v-10.1.1/seL4/manual/tools/libsel4_tools/ |
H A D | syscall_stub_gen.py | 95 class Type(object): class in inherits:object 136 Return a new Type class representing a pointer to this 160 class PointerType(Type): 165 Type.__init__(self, base_type.name, wordsize, wordsize) 178 class CapType(Type): 183 Type.__init__(self, name, wordsize, wordsize) 185 class StructType(Type): 190 Type.__init__(self, name, size_bits, wordsize) 199 class BitFieldType(Type): 204 Type [all...] |
/seL4-l4v-10.1.1/HOL4/examples/dev/sw/ |
H A D | preARMSyntax.sml | 37 val ops = list_mk_pair [ mk_thy_const {Name = Assem.print_op op1, Thy = "preARM", Ty = Type `:OPERATOR`}, 44 else if cond1 = NONE then mk_none (Type `:COND`) 46 mk_const(Assem.print_cond cond1, Type `:COND`)), 52 NONE => mk_none (Type `:OFFSET`) 64 mk_none (Type `:EXP`) 66 val s1 = mk_list (List.map to_exp slist, Type `:EXP`); 75 mk_list ([to_exp (#src inst)], Type `:EXP`), 76 mk_none (Type `:OFFSET`) 86 mk_list(List.map mk_stm stms, Type `:INST`), 179 val dst1 = if dst0 = mk_none (Type ` [all...] |
/seL4-l4v-10.1.1/HOL4/examples/dev/sw/working/0.1/ |
H A D | preARMSyntax.sml | 37 val ops = list_mk_pair [ mk_thy_const {Name = Assem.print_op op1, Thy = "preARM", Ty = Type `:OPERATOR`}, 44 else if cond1 = NONE then mk_none (Type `:COND`) 46 mk_const(Assem.print_cond cond1, Type `:COND`)), 52 NONE => mk_none (Type `:OFFSET`) 64 mk_none (Type `:EXP`) 66 val s1 = mk_list (List.map to_exp slist, Type `:EXP`); 75 mk_list ([to_exp (#src inst)], Type `:EXP`), 76 mk_none (Type `:OFFSET`) 86 mk_list(List.map mk_stm stms, Type `:INST`), 179 val dst1 = if dst0 = mk_none (Type ` [all...] |
/seL4-l4v-10.1.1/HOL4/examples/dev/sw/working/0.2/ |
H A D | preARMSyntax.sml | 37 val ops = list_mk_pair [ mk_thy_const {Name = Assem.print_op op1, Thy = "preARM", Ty = Type `:OPERATOR`}, 44 else if cond1 = NONE then mk_none (Type `:COND`) 46 mk_const(Assem.print_cond cond1, Type `:COND`)), 52 NONE => mk_none (Type `:OFFSET`) 64 mk_none (Type `:EXP`) 66 val s1 = mk_list (List.map to_exp slist, Type `:EXP`); 75 mk_list ([to_exp (#src inst)], Type `:EXP`), 76 mk_none (Type `:OFFSET`) 86 mk_list(List.map mk_stm stms, Type `:INST`), 179 val dst1 = if dst0 = mk_none (Type ` [all...] |
/seL4-l4v-10.1.1/isabelle/src/Pure/General/ |
H A D | sql.scala | 61 object Type extends Enumeration 72 def sql_type_default(T: Type.Value): Source = T.toString 74 def sql_type_sqlite(T: Type.Value): Source = 75 if (T == Type.Boolean) "INTEGER" 76 else if (T == Type.Date) "TEXT" 79 def sql_type_postgresql(T: Type.Value): Source = 80 if (T == Type.Bytes) "BYTEA" 89 Column(name, Type.Boolean, strict, primary_key) 91 Column(name, Type.Int, strict, primary_key) 93 Column(name, Type [all...] |
/seL4-l4v-10.1.1/l4v/isabelle/src/Pure/General/ |
H A D | sql.scala | 61 object Type extends Enumeration 72 def sql_type_default(T: Type.Value): Source = T.toString 74 def sql_type_sqlite(T: Type.Value): Source = 75 if (T == Type.Boolean) "INTEGER" 76 else if (T == Type.Date) "TEXT" 79 def sql_type_postgresql(T: Type.Value): Source = 80 if (T == Type.Bytes) "BYTEA" 89 Column(name, Type.Boolean, strict, primary_key) 91 Column(name, Type.Int, strict, primary_key) 93 Column(name, Type [all...] |
/seL4-l4v-10.1.1/HOL4/src/datatype/ |
H A D | ind_types.sml | 30 val (Type,Term) = parse_from_grammars ind_typeTheory.ind_type_grammars value 66 in Term.mk_thy_const{Name=n, Thy=thy, Ty=Type.type_subst theta ty} 70 let val (ty, _) = Type.dom_rng (type_of tm1) 71 val tyins = Type.match_type ty (type_of tm2) 102 This is not the same as Type.type_subst, which only substitutes 169 val aty = Type.alpha 188 handle HOL_ERR _ => Type.bool 214 val conty = itlist (curry Type.-->) (map type_of args) recty 225 val predty = Type.-->(recty, Type [all...] |
/seL4-l4v-10.1.1/HOL4/src/bag/ |
H A D | bagSyntax.sml | 10 val bag_ty = Type.alpha --> num_ty 21 (Type.alpha --> Type.beta) --> (Type.alpha --> num_ty) --> 22 (Type.beta --> num_ty)); 25 (Type.alpha --> bool) --> bag_ty --> bool)
|
/seL4-l4v-10.1.1/HOL4/examples/computability/lambda/ |
H A D | brackabs.sml | 8 val (Type,Term) = parse_from_grammars brackabsTheory.brackabs_grammars value
|