/seL4-l4v-10.1.1/HOL4/Manual/Description/ |
H A D | QuantHeuristics.tex | 306 monochotomy lemma comes from HOL~4's \holtxt{Type\_Base} library. This means that \holtxt{record\_qp} is stateful. 316 \holtxt{Type\_Base}. Such information is not only useful for records
|
H A D | misc.tex | 1595 \item[\texttt{Type}] 1650 @Type{type_id_1,
|
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/Guide/ |
H A D | guide.tex | 209 \item Type `{\tt make clean}' to remove all traces of previous executions of 213 \item Type `{\tt make tutorial}' to typeset the \TUTORIAL\ volume using \latex. 215 \item Type `{\tt make all}' to typeset the \TUTORIAL\ volume completely from 239 \item Type `{\tt make clean}' to remove all traces of previous executions of 244 \item Type `{\tt make description}' to typeset the \DESCRIPTION\ volume using 247 \item Type `{\tt make index}' to create the \DESCRIPTION\ index. This creates 250 \item Type `{\tt make all}' to typeset the \DESCRIPTION\ volume completely from 278 \item Type `{\tt make all}' to create the \LaTeX\ sources for the \REFERENCE\ 325 \item Type `{\tt make clean}' to remove all traces of previous executions of 330 \item Type `{\t [all...] |
/seL4-l4v-10.1.1/HOL4/Manual/Logic/ |
H A D | semantics.tex | 234 \subsubsection*{Type instantiation [{\small\tt INST\_TYPE}]} 1329 (\equant{f_{\alpha\fun\sigma}}{\sf Type\_Definition}\ p\ f)\ \imp\ q 1386 (\Gamma & , & (\equant{f_{\alpha\fun\sigma}}{\sf Type\_Definition}\ 1524 Type\_Definition}\ p\ f)\ \imp\ q )$ is in ${\sf Theorems}_{\cal T}$, 1548 \equant{f_{\alpha\fun\sigma}}{\sf Type\_Definition}\ p\ f 1555 Type\_Definition}\ p\ f$, one has that
|
H A D | syntax.tex | 153 \item {\bf Type variables:}\index{type variables, in HOL logic@type variables, in \HOL{} logic!abstract form of} these stand for arbitrary 172 of arity $n$. Type operators denote operations for constructing sets. 207 \subsection{Type structures}
|
/seL4-l4v-10.1.1/HOL4/Manual/Translations/IT/Description/ |
H A D | QuantHeuristics.tex | 296 monochotomy lemma comes from HOL~4's \holtxt{Type\_Base} library. This means that \holtxt{record\_qp} is stateful. 306 \holtxt{Type\_Base}. Such information is not only useful for records
|
H A D | libraries.tex | 1054 in un'applicazione di \ml{Parse.Type} alla quotation \ml{`:'a -> bool`}. 1166 ! Type clash: expression of type
|
H A D | misc.tex | 1412 \item[\texttt{Type}] 1466 @Type{type_id_1,
|
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
|
H A D | system.tex | 533 Type inference failure: unable to infer a type for the application of 2176 %\subsection{Type abbreviations}\label{typeabbrev}\index{types, nella logica HOL@types, nella logica \HOL{}!abbreviation of}\index{type abbreviations!nella logica HOL@nella logica \HOL{}}\index{abbreviation of types, nella logica HOL@abbreviation of types, nella logica \HOL{}|(} 2188 %if $\sigma$ is polymorphic. Type abbreviations 2249 %Type Abbreviations -- numpair ":num * num" 2282 %Type abbreviations tend to be little used in practice; the antiquotation
|
H A D | theories.tex | 2428 Type & 2437 Type &
|
/seL4-l4v-10.1.1/HOL4/Manual/Translations/IT/Logic/ |
H A D | semantics.tex | 1328 (\equant{f_{\alpha\fun\sigma}}{\sf Type\_Definition}\ p\ f)\ \imp\ q 1385 (\Gamma & , & (\equant{f_{\alpha\fun\sigma}}{\sf Type\_Definition}\ 1523 Type\_Definition}\ p\ f)\ \imp\ q )$ � in ${\sf Theorems}_{\cal T}$, 1547 \equant{f_{\alpha\fun\sigma}}{\sf Type\_Definition}\ p\ f 1554 Type\_Definition}\ p\ f$, si ha che
|
/seL4-l4v-10.1.1/HOL4/Manual/Translations/IT/Tutorial/ |
H A D | combin.tex | 33 \label{sec:Type-Combinators}
|
H A D | logic.tex | 208 Type inference failure: unable to infer a type for the application of 228 Type inference failure: unable to infer a type for the application of
|
/seL4-l4v-10.1.1/HOL4/Manual/Tutorial/ |
H A D | logic.tex | 143 \paragraph{Type checking} 185 \paragraph{Type constraints} 208 Type inference failure: unable to infer a type for the application of 228 Type inference failure: unable to infer a type for the application of
|
/seL4-l4v-10.1.1/HOL4/developers/discussion/ |
H A D | overloading-extension.tex | 120 \section{Type-Recursive Definitions}
|
/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/examples/ARM/v7/ |
H A D | armSyntax.sml | 31 Term.inst [Type.alpha |-> 93 Term.inst [Type.alpha |-> stringSyntax.string_ty] s) 98 [Type.alpha |-> Term.type_of v, 99 Type.beta |-> Term.type_of s] valuestate_tm, [v,s]) 103 HolKernel.mk_comb(Term.inst[Type.alpha |-> Term.type_of t] constT_tm,t) 108 [Type.alpha |-> dest_monad_type (Term.type_of f), 109 Type.beta |-> (dest_monad_type o snd o Type.dom_rng o Term.type_of) g] 115 [Type.alpha |-> dest_monad_type (Term.type_of f), 116 Type [all...] |
H A D | arm_astSyntax.sml | 15 Term.inst [Type.alpha |-> 22 case Lib.total Type.dest_thy_type ty 31 Term.inst [Type.alpha |-> ty]) v) (Lib.zip x y);
|
H A D | arm_stepLib.sml | 16 val (Type,Term) = parse_from_grammars arm_stepTheory.arm_step_grammars value 130 val inst_type2 = Thm.INST_TYPE [Type.alpha |-> ``:2``]; 131 val inst_type32 = Thm.INST_TYPE [Type.alpha |-> ``:32``]; 235 val I_flags_fupd = Term.inst [Type.alpha |-> ``:ARMpsr``] combinSyntax.I_tm 515 (Term.inst [Type.alpha |-> wordsSyntax.dest_word_type (Term.type_of w)]
|
/seL4-l4v-10.1.1/HOL4/examples/ARM_security_properties/ |
H A D | ARM_proverLib.sig | 13 val get_monad_type : Type.hol_type -> Type.hol_type 16 val get_type_inst : Type.hol_type * bool -> Type.hol_type
|
H A D | ARM_prover_extLib.sig | 13 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/examples/ARM_security_properties/model/ |
H A D | armSyntax.sml | 31 Term.inst [Type.alpha |-> 94 Term.inst [Type.alpha |-> stringSyntax.string_ty] s) 99 [Type.alpha |-> Term.type_of v, 100 Type.beta |-> Term.type_of s] valuestate_tm, [v,s]) 104 HolKernel.mk_comb(Term.inst[Type.alpha |-> Term.type_of t] constT_tm,t) 109 [Type.alpha |-> dest_monad_type (Term.type_of f), 110 Type.beta |-> (dest_monad_type o snd o Type.dom_rng o Term.type_of) g] 116 [Type.alpha |-> dest_monad_type (Term.type_of f), 117 Type [all...] |
H A D | arm_astSyntax.sml | 15 Term.inst [Type.alpha |-> 22 case Lib.total Type.dest_thy_type ty 31 Term.inst [Type.alpha |-> ty]) v) (Lib.zip x y);
|