/seL4-l4v-10.1.1/HOL4/src/1/ |
H A D | Abbrev.sig | 5 type hol_type = Type.hol_type
|
H A D | Rsyntax.sml | 6 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 D | gh168cScript.sml | 18 val ty = Parse.Type [QUOTE s]
|
/seL4-l4v-10.1.1/HOL4/src/experimental-kernel/ |
H A D | Type.sml | 1 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 D | PPBackEnd.sig | 4 type hol_type = Type.hol_type
|
H A D | Parse_supportENV.sml | 14 exception AQincompat of { nm : string, aqty : Type.hol_type,
|
H A D | type_grammar.sml | 11 | 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 D | Pretype.sml | 148 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 D | ASCIInumbersLib.sml | 9 val (Type, Term) = value
|
/seL4-l4v-10.1.1/HOL4/polyml/libpolyml/ |
H A D | pecoffexport.cpp | 86 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 D | term_xml.scala | 22 { 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 D | term_xml.scala | 22 { 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 D | binary_ieeeSyntax.sml | 12 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 D | OpenTheoryCommon.sml | 24 | 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 D | holfootSyntax.sml | 27 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 D | options.scala | 19 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 D | options.scala | 19 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 D | Import.sml | 109 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 D | updateLib.sml | 9 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 D | arm_configLib.sml | 15 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 D | types0.tex | 11 \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 D | types0.tex | 11 \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 D | mechReasoning.sml | 75 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 D | arm_core_decompLib.sml | 26 val vars = Term.mk_var ("cond", Type.bool) ::
|
/seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/lib/ |
H A D | Nat.sig | 3 (* Type should be abstract when not using SMLExport, i.e.
|