| /seL4-l4v-10.1.1/HOL4/src/num/reduce/Manual/ |
| H A D | Makefile | 2 # Make the manual for the "reduce" library #
13 all:; make clean; make ids; make reduce; make index; make reduce ps pdf
19 echo "\chapter{ML Functions in the reduce Library}" >entries.tex
24 ${MAKEINDEX} reduce.idx
26 reduce:
27 latex reduce.tex
30 dvips reduce.dvi -o
33 pdflatex reduce.tex
|
| H A D | description.tex | 1 \chapter{The reduce Library}
3 This manual describes the use of the \ml{reduce} library, as well as discussing
12 tediousness. However, using the \ml{reduce} library, the evaluation of:
42 The \ml{reduce} library uses only the above conversion, together with certain
94 load_library `reduce`;;
|
| /seL4-l4v-10.1.1/HOL4/src/metis/ |
| H A D | mlibRewrite.sig | 29 (* Inter-reduce the equations in the system *)
31 val reduce' : rewrs -> rewrs * int list (* also returns new redexes *)
32 val reduce : rewrs -> rewrs value
|
| H A D | mlibRewrite.sml | 286 (* Inter-reduce the equations in the system *)
419 fun reduce' rw =
427 val _ = chatrewrs "reduce before" rw
428 val _ = chatrewrs "reduce after" rw'
429 val () = assert (not m) (Bug "reduce: not fully reduced")
434 val reduce = fst o reduce'; value
|
| /seL4-l4v-10.1.1/HOL4/tools/mlyacc/src/ |
| H A D | mklrtable.sml | 98 in say_error(rr,"reduce/reduce conflict");
99 say_error(sr,"shift/reduce conflict");
118 shift/reduce:
121 precedence, a shift/reduce conflict is reported.
128 shift nor the reduce is chosen.
130 reduce/reduce:
132 A reduce/reduce conflic
[all...] |
| H A D | verbose.sml | 75 print ": reduce/reduce conflict between rule ";
85 print ": shift/reduce conflict ";
88 print ", reduce by rule ";
|
| /seL4-l4v-10.1.1/HOL4/src/quotient/examples/lambda/ |
| H A D | barendregt.sig | 4 (* DESCRIPTION : Tactic to reduce proper substitution to the much *)
|
| /seL4-l4v-10.1.1/HOL4/src/quotient/examples/sigma/ |
| H A D | barendregt.sig | 4 (* DESCRIPTION : Tactic to reduce proper substitution to the much *)
|
| /seL4-l4v-10.1.1/seL4/tools/ |
| H A D | umm.py | 18 from functools import reduce namespace
55 return (reduce(fold, xs, ([], [])))[0]
99 return (reduce(lambda x, y: x + y, res))
|
| /seL4-l4v-10.1.1/isabelle/src/Tools/Metis/src/ |
| H A D | Units.sig | 47 val reduce : units -> Rule.rule value
|
| H A D | Rewrite.sig | 82 (* Inter-reduce the equations in the system. *)
85 val reduce' : rewrite -> rewrite * equationId list
87 val reduce : rewrite -> rewrite value
|
| H A D | Active.sig | 15 reduce : bool,
|
| H A D | Clause.sig | 81 val reduce : Units.units -> clause -> clause value
|
| /seL4-l4v-10.1.1/l4v/isabelle/src/Tools/Metis/src/ |
| H A D | Units.sig | 47 val reduce : units -> Rule.rule value
|
| H A D | Rewrite.sig | 82 (* Inter-reduce the equations in the system. *)
85 val reduce' : rewrite -> rewrite * equationId list
87 val reduce : rewrite -> rewrite value
|
| H A D | Active.sig | 15 reduce : bool,
|
| H A D | Clause.sig | 81 val reduce : Units.units -> clause -> clause value
|
| /seL4-l4v-10.1.1/HOL4/examples/formal-languages/context-free/ |
| H A D | precparserScript.sml | 51 reduce : 'trm -> 'tok -> 'trm -> 'trm option ;
65 OPTION_MAP (��r. (INR r :: rest, [])) (pM.reduce tm1 opn tm2)
75 (pM.reduce tm1 opn tm2)
162 val reduce = ``��tm1 c tm2. if c = #"*" then SOME (Times tm1 tm2)
167 reduce := ^reduce ;
|
| /seL4-l4v-10.1.1/HOL4/examples/pgcl/src/ |
| H A D | posrealTools.sig | 22 val posreal_reduce_ss : simpLib.simpset (* reduce + posreal_reduce *)
|
| /seL4-l4v-10.1.1/isabelle/src/Doc/Tutorial/document/ |
| H A D | documents0.tex | 17 reduce the mental effort to comprehend and apply them.
|
| /seL4-l4v-10.1.1/l4v/isabelle/src/Doc/Tutorial/document/ |
| H A D | documents0.tex | 17 reduce the mental effort to comprehend and apply them.
|
| /seL4-l4v-10.1.1/HOL4/src/compute/examples/ |
| H A D | Arith.sml | 39 * strongly (arg of a free var), but we will have to reduce the
112 reduce `2 EXP 128`; (* 10.5 *)
|
| /seL4-l4v-10.1.1/HOL4/examples/acl2/examples/M1/ |
| H A D | complex_rationalScript.sml | 203 `reduce(x,y) =
211 `reduced_nmr r = FST(reduce(rep_frac(rep_rat r)))`;
218 `reduced_dnm r = SND(reduce(rep_frac(rep_rat r)))`;
|
| /seL4-l4v-10.1.1/HOL4/examples/acl2/examples/acl2-hol-ltl-paper-example/ |
| H A D | complex_rationalScript.sml | 203 `reduce(x,y) =
211 `reduced_nmr r = FST(reduce(rep_frac(rep_rat r)))`;
218 `reduced_dnm r = SND(reduce(rep_frac(rep_rat r)))`;
|
| /seL4-l4v-10.1.1/HOL4/examples/acl2/ml/ |
| H A D | complex_rationalScript.sml | 203 `reduce(x,y) =
211 `reduced_nmr r = FST(reduce(rep_frac(rep_rat r)))`;
218 `reduced_dnm r = SND(reduce(rep_frac(rep_rat r)))`;
|