/seL4-l4v-master/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-master/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-master/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-master/HOL4/src/quotient/examples/lambda/ |
H A D | barendregt.sig | 4 (* DESCRIPTION : Tactic to reduce proper substitution to the much *)
|
/seL4-l4v-master/HOL4/src/quotient/examples/sigma/ |
H A D | barendregt.sig | 4 (* DESCRIPTION : Tactic to reduce proper substitution to the much *)
|
/seL4-l4v-master/seL4/tools/ |
H A D | umm.py | 11 from functools import reduce namespace 51 return (reduce(fold, xs, ([], [])))[0] 101 return (reduce(lambda x, y: x + y, res))
|
/seL4-l4v-master/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-master/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-master/HOL4/examples/formal-languages/context-free/ |
H A D | precparserScript.sml | 49 reduce : 'trm -> 'tok -> 'trm -> 'trm option ; 63 OPTION_MAP (��r. (INR r :: rest, [])) (pM.reduce tm1 opn tm2) 73 (pM.reduce tm1 opn tm2) 160 val reduce = ``��tm1 c tm2. if c = #"*" then SOME (Times tm1 tm2) 165 reduce := ^reduce ;
|
/seL4-l4v-master/HOL4/examples/pgcl/src/ |
H A D | posrealTools.sig | 22 val posreal_reduce_ss : simpLib.simpset (* reduce + posreal_reduce *)
|
/seL4-l4v-master/isabelle/src/Doc/Tutorial/document/ |
H A D | documents0.tex | 17 reduce the mental effort to comprehend and apply them.
|
/seL4-l4v-master/l4v/isabelle/src/Doc/Tutorial/document/ |
H A D | documents0.tex | 17 reduce the mental effort to comprehend and apply them.
|
/seL4-l4v-master/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-master/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-master/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-master/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)))`;
|