Searched refs:Type (Results 176 - 200 of 497) sorted by relevance

1234567891011>>

/seL4-l4v-10.1.1/HOL4/src/parse/
H A DPreterm.sig4 type hol_type = Type.hol_type
H A Dtype_pp.sml4 open Feedback Type Portable HOLgrammars type_grammar
318 p (Type`:(bool,num)fmap`)
H A DOverload.sml18 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 Dselftest.sml1 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 DHolKernelDoc.sig6 type hol_type = Type.hol_type
/seL4-l4v-10.1.1/HOL4/src/quotient/examples/
H A Dtactics.sig21 type hol_type = Type.hol_type
/seL4-l4v-10.1.1/HOL4/src/ring/src/
H A Dquote.sml9 val (Type,Term) = parse_from_grammars quoteTheory.quote_grammars value
/seL4-l4v-10.1.1/HOL4/src/simp/src/
H A DCond_rewr.sml47 | 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 DsyntaxScript.sml52 val () = type_abbrev ("state", Type `:string -> 'a`);
/seL4-l4v-10.1.1/HOL4/developers/
H A DgenerateBuildSummary.sml39 \Content-Type: text/plain; charset=UTF-8\n\
/seL4-l4v-10.1.1/HOL4/polyml/mlsource/MLCompiler/
H A DEXPORTTREESIG.sml32 val PTtype: types -> ptProperties (* Type of an expression *)
/seL4-l4v-10.1.1/isabelle/src/Doc/Logics/document/
H A Dpreface.tex33 \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 Dpreface.tex33 \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 DregexpSyntax.sml104 (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 Darm_progLib.sml10 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 Darm_progScript.sml136 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 Dm0_core_decompLib.sml31 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 Driscv_stepLib.sml13 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 DboolLib.sml34 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 DalignmentScript.sml78 |> Thm.INST_TYPE [Type.beta |-> Type.alpha]
/seL4-l4v-10.1.1/HOL4/examples/lambda/other-models/
H A DncScript.sml269 (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 Dsyntax.tex46 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 Dsyntax.tex46 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 Dapi.tex35 \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 Ddefunctionalize.sml48 #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" *)

Completed in 217 milliseconds

1234567891011>>