/seL4-l4v-10.1.1/HOL4/src/parse/ |
H A D | Preterm.sig | 4 type hol_type = Type.hol_type
|
H A D | type_pp.sml | 4 open Feedback Type Portable HOLgrammars type_grammar 318 p (Type`:(bool,num)fmap`)
|
H A D | Overload.sml | 18 type overloaded_op_info = {base_type : Type.hol_type, actual_ops : term list, 19 tyavoids : Type.hol_type list} 96 open stmonad Lib Type 203 val ty1_gte_ty2 = Lib.can (Type.match_type ty1) ty2 204 val ty2_gte_ty1 = Lib.can (Type.match_type ty2) ty1
|
H A D | selftest.sml | 1 open Lib Type PP smpp PPBackEnd testutils 78 add_ann_string ("Type variable", TyV) >> 85 Ty = (Type.bool, fn () => "bool")}) >> 400 val bool = Type.bool 401 val alpha = Type.alpha
|
/seL4-l4v-10.1.1/HOL4/src/postkernel/ |
H A D | HolKernelDoc.sig | 6 type hol_type = Type.hol_type
|
/seL4-l4v-10.1.1/HOL4/src/quotient/examples/ |
H A D | tactics.sig | 21 type hol_type = Type.hol_type
|
/seL4-l4v-10.1.1/HOL4/src/ring/src/ |
H A D | quote.sml | 9 val (Type,Term) = parse_from_grammars quoteTheory.quote_grammars value
|
/seL4-l4v-10.1.1/HOL4/src/simp/src/ |
H A D | Cond_rewr.sml | 47 | SOME n => ((("", ""), ~n), Type.alpha) 51 | COMB _ => ((("", ""), 3), Type.alpha) (* should never happen *) 55 lex_cmp Type.compare) 69 case Type.compare(type_of bv1, type_of bv2) of
|
/seL4-l4v-10.1.1/HOL4/examples/pgcl/src/ |
H A D | syntaxScript.sml | 52 val () = type_abbrev ("state", Type `:string -> 'a`);
|
/seL4-l4v-10.1.1/HOL4/developers/ |
H A D | generateBuildSummary.sml | 39 \Content-Type: text/plain; charset=UTF-8\n\
|
/seL4-l4v-10.1.1/HOL4/polyml/mlsource/MLCompiler/ |
H A D | EXPORTTREESIG.sml | 32 val PTtype: types -> ptProperties (* Type of an expression *)
|
/seL4-l4v-10.1.1/isabelle/src/Doc/Logics/document/ |
H A D | preface.tex | 33 \item[\thydx{CTT}] is a version of Martin-L\"of's Constructive Type
|
/seL4-l4v-10.1.1/l4v/isabelle/src/Doc/Logics/document/ |
H A D | preface.tex | 33 \item[\thydx{CTT}] is a version of Martin-L\"of's Constructive Type
|
/seL4-l4v-10.1.1/HOL4/examples/formal-languages/regular/ |
H A D | regexpSyntax.sml | 104 (listSyntax.mk_nil Type.bool) bv 123 (listSyntax.mk_nil Type.bool) ml_bitlist
|
/seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/arm/prog/ |
H A D | arm_progLib.sml | 10 val (Type, Term) = parse_from_grammars arm_progTheory.arm_prog_grammars value 110 (List.concat (List.map dest_opc l), Type.bool), ty32) 592 val v3 = Term.mk_var ("x3", Type.bool) 593 val v4 = Term.mk_var ("x4", Type.bool) 594 val v5 = Term.mk_var ("x5", Type.bool) 595 val v6 = Term.mk_var ("x6", Type.bool) 596 val vn = listSyntax.mk_list ([v3, v4, v5, v6], Type.bool) 843 val opc = listSyntax.mk_list (!rev_endian i, Type.bool)
|
H A D | arm_progScript.sml | 136 else Term.mk_var (s ^ Int.toString i, Type.bool)) 138 (listSyntax.mk_list (List.rev l, Type.bool), ``:32``))
|
/seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/m0/decompiler/ |
H A D | m0_core_decompLib.sml | 31 tripleSyntax.get_component (Lib.equal (Term.mk_var ("cond'", Type.bool))) 195 val vars = Term.mk_var ("cond", Type.bool) ::
|
/seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/riscv/step/ |
H A D | riscv_stepLib.sml | 13 val (Type, Term) = parse_from_grammars riscv_stepTheory.riscv_step_grammars value 33 val () = ignore (ty = Type.bool andalso List.length l <= 32 orelse
|
/seL4-l4v-10.1.1/HOL4/src/1/ |
H A D | boolLib.sml | 34 val (Type,Term) = parse_from_grammars bool_grammars value 209 else if Type.compare(type_of v1,type_of v2) = EQUAL then
|
/seL4-l4v-10.1.1/HOL4/src/n-bit/ |
H A D | alignmentScript.sml | 78 |> Thm.INST_TYPE [Type.beta |-> Type.alpha]
|
/seL4-l4v-10.1.1/HOL4/examples/lambda/other-models/ |
H A D | ncScript.sml | 269 (INST_TYPE [beta |-> Type`:bool#bool`] nc_ITERATOR) 353 let val instth = INST_TYPE [beta |-> Type`:'a nc # 'b`] nc_ITERATOR 390 val instth = INST_TYPE [beta |-> Type`:'a nc`] nc_ITERATOR 444 val v1 = genvar (Type`:'a nc -> 'a nc`) 445 and v2 = genvar (Type`:'a nc -> 'b`) 504 let val instth = INST_TYPE [beta |-> Type`:string->'a nc`] nc_RECURSION 584 let val instth = INST_TYPE [Type.beta |-> Type.bool] nc_RECURSION
|
/seL4-l4v-10.1.1/HOL4/Manual/Description/ |
H A D | syntax.tex | 46 Type constants are also known as type operators. They must be 47 alphanumeric. Type variables are alphanumerics written with a leading
|
/seL4-l4v-10.1.1/HOL4/Manual/Translations/IT/Description/ |
H A D | syntax.tex | 46 Type constants are also known as type operators. They must be 47 alphanumeric. Type variables are alphanumerics written with a leading
|
/seL4-l4v-10.1.1/seL4/manual/parts/ |
H A D | api.tex | 35 \textbf{Type} & \textbf{Name} & \textbf{Description} \\ 196 \ipcbloc{IPCBuffer[1]} & Type of lookup failure\\
|
/seL4-l4v-10.1.1/HOL4/examples/dev/sw2/ |
H A D | defunctionalize.sml | 48 #1 (Type.dest_type (type_of t)) = "fun" 173 handle e => #1 (Type.dest_type t) 181 handle e => #1 (Type.dest_type (type_of arg))}) 244 val f_index = String.extract (#1 (Type.dest_type clos_type), 4, NONE) (* take the value of n from "closn" *) 265 val f_index = String.extract (#1 (Type.dest_type clos_type), 4, NONE) (* take the value of n from "closn" *)
|