Searched refs:Type (Results 51 - 75 of 497) sorted by relevance

1234567891011>>

/seL4-l4v-10.1.1/HOL4/src/1/
H A DAbbrev.sig5 type hol_type = Type.hol_type
H A DRsyntax.sml6 type hol_type = Type.hol_type;
9 fun mk_type{Tyop,Args} = Type.mk_type(Tyop,Args)
26 fun dest_type ty = let val (s,l) = Type.dest_type ty in {Tyop=s,Args=l} end
/seL4-l4v-10.1.1/HOL4/src/1/theory_tests/
H A Dgh168cScript.sml18 val ty = Parse.Type [QUOTE s]
/seL4-l4v-10.1.1/HOL4/src/experimental-kernel/
H A DType.sml1 structure Type :> Type = structure
9 val WARN = HOL_WARNING "Type";
10 fun ERR f msg = HOL_ERR {origin_structure = "Type",
50 | dest_vartype _ = raise ERR "dest_vartype" "Type not a vartype"
87 fun dest_type (Tyv _) = raise ERR "dest_type" "Type a variable"
104 fun dest_thy_type (Tyv _) = raise ERR "dest_thy_type" "Type a variable"
155 fun dom_rng (Tyv _) = raise ERR "dom_rng" "Type a variable"
158 "Type not a function type"
/seL4-l4v-10.1.1/HOL4/src/parse/
H A DPPBackEnd.sig4 type hol_type = Type.hol_type
H A DParse_supportENV.sml14 exception AQincompat of { nm : string, aqty : Type.hol_type,
H A Dtype_grammar.sml11 | TYOP {Thy, Tyop, Args} => isSome (Type.op_arity {Thy = Thy, Tyop = Tyop})
87 fun default_typrinter (G:grammar) (ty:Type.hol_type) =
106 Type.mk_thy_type {Thy = Thy, Tyop = Tyop,
108 | PARAM n => Type.mk_vartype ("'"^str (chr (n + ord #"a")))
174 open Type Theory
176 case Type.op_arity {Tyop = name, Thy = thy} of
277 open Type
278 val params = Listsort.sort Type.compare (type_vars ty)
281 (0, Binarymap.mkDict Type.compare) params
388 can (Type
[all...]
H A DPretype.sml148 if Type.is_vartype t then Vartype (Type.dest_vartype t)
149 else let val {Tyop = tyop, Args, Thy} = Type.dest_thy_type t
182 Vartype s => Type.mk_vartype s
184 Type.mk_thy_type{Tyop = s, Thy = Thy, Args = map clean Args}
187 fun toTypeM ty : Type.hol_type in_env =
258 case Type.decls tyop of
/seL4-l4v-10.1.1/HOL4/src/string/
H A DASCIInumbersLib.sml9 val (Type, Term) = value
/seL4-l4v-10.1.1/HOL4/polyml/libpolyml/
H A Dpecoffexport.cpp86 reloc.Type = DIRECT_WORD_RELOCATION;
109 reloc.Type = DIRECT_WORD_RELOCATION;
140 symbol.Type = symType;
179 reloc.Type = RELATIVE_32BIT_RELOCATION;
181 reloc.Type = DIRECT_WORD_RELOCATION;
310 reloc.Type = DIRECT_WORD_RELOCATION;
317 reloc.Type = DIRECT_WORD_RELOCATION;
326 reloc.Type = DIRECT_WORD_RELOCATION;
/seL4-l4v-10.1.1/isabelle/src/Pure/
H A Dterm_xml.scala22 { case Type(a, b) => (List(a), list(typ)(b)) },
44 { case (List(a), b) => Type(a, list(typ)(b)) },
/seL4-l4v-10.1.1/l4v/isabelle/src/Pure/
H A Dterm_xml.scala22 { case Type(a, b) => (List(a), list(typ)(b)) },
44 { case (List(a), b) => Type(a, list(typ)(b)) },
/seL4-l4v-10.1.1/HOL4/src/floating-point/
H A Dbinary_ieeeSyntax.sml12 Type.mk_thy_type {Thy = "binary_ieee", Tyop = "float_value", Args = []}
15 Type.mk_thy_type {Thy = "binary_ieee", Tyop = "rounding", Args = []}
18 Type.mk_thy_type {Thy = "binary_ieee", Tyop = "flags", Args = []}
21 Type.mk_thy_type {Thy = "binary_ieee", Tyop = "float_compare", Args = []}
24 Type.mk_thy_type {Thy = "binary_ieee", Tyop = "float", Args = [t, w]}
27 Type.mk_thy_type {Thy = "binary_ieee", Tyop = "fp_op", Args = [t, w]}
30 case Type.dest_thy_type ty of
35 case Type.dest_thy_type ty of
/seL4-l4v-10.1.1/HOL4/src/opentheory/
H A DOpenTheoryCommon.sml24 | OType of Type.hol_type
47 | c (OType x1, OType x2) = Type.compare (x1,x2)
/seL4-l4v-10.1.1/HOL4/examples/separationLogic/src/holfoot/
H A DholfootSyntax.sml27 val holfoot_heap_ty = Type `:holfoot_heap`;
28 val holfoot_stack_ty = Type `:holfoot_stack`;
29 val holfoot_state_ty = Type `:holfoot_state`;
30 val holfoot_var_ty = Type `:holfoot_var`;
31 val holfoot_tag_ty = Type `:holfoot_tag`;
32 val holfoot_a_expression_ty = Type `:holfoot_a_expression`;
33 val holfoot_a_proposition_ty = Type `:holfoot_a_proposition`;
78 val var_term = variant (free_vars term) (mk_var (var, Type `:holfoot_var`));
/seL4-l4v-10.1.1/isabelle/src/Pure/System/
H A Doptions.scala19 sealed abstract class Type
23 case object Bool extends Type
24 case object Int extends Type
25 case object Real extends Type
26 case object String extends Type
27 case object Unknown extends Type
33 typ: Type,
222 private def check_type(name: String, typ: Options.Type): Options.Opt =
232 private def put[A](name: String, typ: Options.Type, value: String): Options =
238 private def get[A](name: String, typ: Options.Type, pars
[all...]
/seL4-l4v-10.1.1/l4v/isabelle/src/Pure/System/
H A Doptions.scala19 sealed abstract class Type
23 case object Bool extends Type
24 case object Int extends Type
25 case object Real extends Type
26 case object String extends Type
27 case object Unknown extends Type
33 typ: Type,
222 private def check_type(name: String, typ: Options.Type): Options.Opt =
232 private def put[A](name: String, typ: Options.Type, value: String): Options =
238 private def get[A](name: String, typ: Options.Type, pars
[all...]
/seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/common/
H A DImport.sml109 fun typevar s = Type.mk_vartype ("'" ^ s)
235 val typ = Type.--> (Term.type_of tm, Ty ty)
268 fun bVar v = Term.mk_var (v, Type.bool)
331 val cons = Term.inst [Type.alpha |-> ty] listSyntax.cons_tm
344 case Lib.total Type.dom_rng ty of
408 val typ = Type.--> (Type.--> (fty, fty), Type.--> (rty, rty))
653 val name = fst (Type.dest_type ty)
679 val name = fst (Type
[all...]
/seL4-l4v-10.1.1/HOL4/src/update/
H A DupdateLib.sml9 val (Type,Term) = parse_from_grammars updateTheory.update_grammars value
287 val ok1 = Lib.can (Type.match_type ty)
288 val ok2 = Lib.can (Type.match_type (ty --> ty))
343 ord |> Term.type_of |> Type.dom_rng |> fst |> pairSyntax.dest_prod
349 val c_form = Lib.can (Type.match_type ty3) ty andalso is_c_expr tm
352 Lib.can (Type.match_type (ty3 --> ty3)) ty andalso is_o_expr tm
385 val (uty, oty) = Type.dom_rng (Term.type_of f)
386 val _ = Type.match_type (Term.type_of ord) (oty --> oty --> Type.bool)
412 val fty = pairSyntax.mk_prod (numSyntax.num, Type
[all...]
/seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/arm/step/
H A Darm_configLib.sml15 val (Type, Term) = parse_from_grammars armTheory.arm_grammars value
24 val st = Term.mk_var ("s", Type.mk_type ("arm_state", []))
27 fun mk_arm_type n = Type.mk_thy_type {Thy = "arm", Tyop = n, Args = []}
/seL4-l4v-10.1.1/isabelle/src/Doc/Tutorial/document/
H A Dtypes0.tex11 \item Type classes: how to specify and reason about axiomatic collections of
31 \section{Type Classes} %%%Section
51 specifications involving type classes. Type classes are covered more
/seL4-l4v-10.1.1/l4v/isabelle/src/Doc/Tutorial/document/
H A Dtypes0.tex11 \item Type classes: how to specify and reason about axiomatic collections of
31 \section{Type Classes} %%%Section
51 specifications involving type classes. Type classes are covered more
/seL4-l4v-10.1.1/HOL4/examples/dev/sw/working/0.1/
H A DmechReasoning.sml75 mk_var ("v" ^ (i := !i + 1; Int.toString (!i)) , Type `:DATA`)
149 List.map (fn exp => (i := !i + 1; {redex = exp, residue = mk_var ("v" ^ (Int.toString (!i)), Type `:DATA`)})) expL
177 if type_of t = Type `:DOPER` then true
247 val blk = mk_comb (Term`BLK`, mk_list (List.map IRSyntax.convert_stm stms, Type`:DOPER`));
248 val st = mk_pair (mk_var ("regs", Type `:REGISTER |-> DATA`), mk_var ("mem", Type `:ADDR |-> DATA`));
297 val st' = mk_var ("st", Type `:DSTATE`);
340 val ir_abbr = mk_var ("ir", Type `:CTL_STRUCTURE`);
411 val ir_abbr = mk_var ("ir", Type `:CTL_STRUCTURE`);
412 val st = mk_var ("st", Type `
[all...]
/seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/arm/decompiler/
H A Darm_core_decompLib.sml26 val vars = Term.mk_var ("cond", Type.bool) ::
/seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/lib/
H A DNat.sig3 (* Type should be abstract when not using SMLExport, i.e.

Completed in 383 milliseconds

1234567891011>>