/seL4-l4v-master/HOL4/examples/acl2/ml/ |
H A D | extendTranslateScript.sml | 1340 val LIST_UNZIP = prove(``pair (list f) (list g) (UNZIP l) = 1341 cons (strip_cars (list (pair f g) l)) (strip_cdrs (list (pair f g) l))``, 1369 (list (pair f g) (ZIP (l1,l2)) = pairlist (list f l1) (list g l2))``,
|
/seL4-l4v-master/HOL4/src/integer/ |
H A D | IntDP_Munge.sml | 37 (* returns a list of pairs, where the first element of each pair is a non-
|
/seL4-l4v-master/HOL4/src/HolSmt/ |
H A D | SmtLib.sml | 58 (* (HOL term, a function that maps a pair (rator, rands) to an
|
/seL4-l4v-master/HOL4/examples/algebra/field/ |
H A D | symmetryFieldScript.sml | 537 Given a field/subfield pair: s <<= r,
|
/seL4-l4v-master/HOL4/src/compute/src/ |
H A D | clauses.sml | 208 as a pair `(const_name, theory_name)`.
|
/seL4-l4v-master/HOL4/src/parse/ |
H A D | Overload.sml | 21 (* the overload info is thus a pair:
|
/seL4-l4v-master/HOL4/src/quotient/examples/lambda/ |
H A D | alphaScript.sml | 54 (* matching function, that checks if a pair of variables match according *) 55 (* to a given pair of lists of variables; the lists are searched, and *)
|
/seL4-l4v-master/isabelle/src/Doc/Tutorial/document/ |
H A D | sets.tex | 463 Note also that we can write \isa{f(x:=z)} with only one pair of parentheses 860 Now that \isa{x} has been replaced by the pair \isa{(a,b)}, we can
|
/seL4-l4v-master/l4v/isabelle/src/Doc/Tutorial/document/ |
H A D | sets.tex | 463 Note also that we can write \isa{f(x:=z)} with only one pair of parentheses 860 Now that \isa{x} has been replaced by the pair \isa{(a,b)}, we can
|
/seL4-l4v-master/HOL4/src/coalgebras/ |
H A D | pathScript.sml | 1181 (Q.ISPEC `\pair. let pullapart g p = (first p, 1186 case pair of
|
/seL4-l4v-master/HOL4/src/probability/ |
H A D | martingaleScript.sml | 735 !A B. prod_sigma A B = general_sigma pair$, A B 869 >> MP_TAC (Q.SPECL [���pair$,���, ���X���, ���Y���, ���A���, ���B���, ���f���, ���g���] 1129 >> MP_TAC (Q.SPECL [���pair$,���, ���FST���, ���SND���, ���X���, ���Y���, ���E���, ���G���] 1241 >> MP_TAC (Q.SPECL [���pair$,���,���FST���,���SND���,���X���,���Y���,���E���,���G���,���A���,���B���,���u���,���v���,���m���,���m'���] 1322 >> MP_TAC (Q.SPECL [���pair$,���,���FST���,���SND���,���X���,���Y���,���A���,���B���,���u���,���v���,���m���,���m'���] 2527 >> MP_TAC (Q.SPECL [���pair$,���,���FST���,���SND���,���X���,���Y���,���A���,���B���,���u���,���v���,���m0���]
|
/seL4-l4v-master/HOL4/src/quotient/Manual/ |
H A D | quotient.tex | 600 pair & {\tt \#\#\# : } & {\tt ('a -> 'a -> bool) -> ('b -> 'b -> bool) ->} \\ 670 Since the pair and sum relation operators have two arguments, 686 {\tt pair\_equiv} & {\tt : thm -> thm -> thm} \\ 1609 {\tt pair\_quotient} & {\tt : thm -> thm -> thm} \\ 1698 pair & {\tt \#\# : } & {\tt ('a -> 'b) -> ('c -> 'd) ->} \\ 2763 to the list, pair, sum, option, and function type operators, along with 5136 first as the right part of a pair type, and then as the element type of 5437 Furthermore, because the {\tt let} involves a pair, the 5438 pair is implemented by the {\tt UNCURRY} operator, which is also higher-order.
|
/seL4-l4v-master/l4v/isabelle/src/Doc/Nitpick/document/ |
H A D | root.tex | 646 the integer type \textit{my\_int} by encoding the integer $x$ by a pair of 677 that converts the pair notation to the standard mathematical notation: 1974 is approximated by a subset of the possible function or pair values. 2626 unregistering postprocessors consists of the following pair of functions defined 2650 pair of functions defined in the \textit{Nitpick\_HOL} structure:
|
/seL4-l4v-master/isabelle/src/Doc/Nitpick/document/ |
H A D | root.tex | 646 the integer type \textit{my\_int} by encoding the integer $x$ by a pair of 677 that converts the pair notation to the standard mathematical notation: 1974 is approximated by a subset of the possible function or pair values. 2626 unregistering postprocessors consists of the following pair of functions defined 2650 pair of functions defined in the \textit{Nitpick\_HOL} structure:
|
/seL4-l4v-master/HOL4/Manual/Description/ |
H A D | HolBdd.tex | 655 The integer returned as the first component of the pair is a pointer 960 A finalized value, in the \mosml{} runtime system, is a pair where the 2258 A state of the iteration is a pair (tb,tb') consisting of the
|
/seL4-l4v-master/HOL4/Manual/Translations/IT/Description/ |
H A D | HolBdd.tex | 655 The integer returned as the first component of the pair is a pointer 960 A finalized value, in the \mosml{} runtime system, is a pair where the 2258 A state of the iteration is a pair (tb,tb') consisting of the
|
/seL4-l4v-master/HOL4/examples/AKS/theories/ |
H A D | AKSintroScript.sml | 1390 Step 1: get a field/subfield pair 1542 Step 1: get a field/subfield pair 2144 Step 1: get a field/subfield pair
|
/seL4-l4v-master/HOL4/src/1/ |
H A D | Drule.sml | 2443 * Take an AC pair, normalize them, then prove left-commutativity * 2456 (* Classify a pair of theorems as one assoc. thm and one comm. thm. Then 2457 return pair (A,C) where A has the form |- f(x,f(y,z)) = f(f(x,y),z) *)
|
H A D | Pmatch.sml | 643 val constrs_type = map (pair (type_of arg)) constrs
|
/seL4-l4v-master/HOL4/examples/algebra/lib/ |
H A D | helperFunctionScript.sml | 625 For the first pair: x <= x. 626 For the second pair: f x <= g x, as g is cover. 627 For the third pair: f (f x) <= g (f x) by g is cover,
|
/seL4-l4v-master/HOL4/src/n-bit/ |
H A D | wordsLib.sml | 493 |> List.map (fn (thy, l) => List.map (Lib.pair thy) l) 499 (s, map (pair "words") 503 map (pair "arithmetic")
|
/seL4-l4v-master/HOL4/examples/l3-machine-code/arm8/model/ |
H A D | arm8.sml | 2451 (acctype,(excl,(pair,(rn_unknown,(rt_unknown,(s,(n,(t,t2)))))))))) = 2452 if pair 2478 (size,(memop,(acctype,(excl,(pair,(Rs,(Rn,(Rt,Rt2)))))))) = 2481 if (memop = MemOp_LOAD) andalso (pair andalso (Rt = Rt2)) 2489 (pair andalso (Rs = Rt2)) 2521 (excl,(pair,(rn_unknown,(rt_unknown,(Rs,(Rn,(Rt,Rt2)))))))))) 5360 val pair = (BitsN.fromBitstring([o1'0],1)) = (BitsN.B(0x1,1)) value 5367 (pair,
|
/seL4-l4v-master/HOL4/polyml/mlsource/MLCompiler/CodeTree/ |
H A D | CODETREE_OPTIMISER.sml | 732 (* Return the pair of functions. *) 920 an argument is a function with tupled or curried arguments into a pair
|
/seL4-l4v-master/HOL4/src/datatype/mutrec/ |
H A D | ConsThms.sml | 442 a pair consisting of the definition of the function and the name of
|
/seL4-l4v-master/HOL4/src/meson/src/ |
H A D | mesonLib.sml | 559 then failwith "repetition of demigoal pair"
|