Searched refs:Type (Results 26 - 50 of 497) sorted by relevance

1234567891011>>

/seL4-l4v-10.1.1/HOL4/examples/ARM_security_properties/
H A DARM_prover_extLib.sig13 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 DThyDataSexp.sml13 | 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 DPsyntax.sml6 val mk_type = Type.mk_type
7 val dest_type = Type.dest_type
H A DAbbrev.sml5 type hol_type = Type.hol_type
/seL4-l4v-10.1.1/HOL4/src/parse/
H A Dparse_type.sig22 val ty_antiq : Type.hol_type -> term
23 val dest_ty_antiq : term -> Type.hol_type
H A DTypeNet.sig6 type hol_type = Type.hol_type
H A DParseDatatype.sig10 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 Dterm.scala20 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 Dterm.scala20 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 Dgh168bScript.sml16 val ty = Parse.Type [QUOTE s]
/seL4-l4v-10.1.1/HOL4/src/TeX/
H A DmungeTools.sig4 datatype command = Theorem | Term | Type
/seL4-l4v-10.1.1/HOL4/src/opentheory/
H A DOpenTheoryCommon.sig12 | OType of Type.hol_type
/seL4-l4v-10.1.1/HOL4/src/n-bit/
H A DfcpSyntax.sml28 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 DbackgroundLib.sig32 val dest_sum_type : Type.hol_type -> Type.hol_type * Type.hol_type
/seL4-l4v-10.1.1/HOL4/examples/muddy/
H A Dfdd.sig21 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 Dsyscall_stub_gen.py95 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 Dsyscall_stub_gen.py95 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 DpreARMSyntax.sml37 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 DpreARMSyntax.sml37 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 DpreARMSyntax.sml37 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 Dsql.scala61 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 Dsql.scala61 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 Dind_types.sml30 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 DbagSyntax.sml10 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 Dbrackabs.sml8 val (Type,Term) = parse_from_grammars brackabsTheory.brackabs_grammars value

Completed in 374 milliseconds

1234567891011>>