Searched refs:plus2 (Results 1 - 11 of 11) sorted by relevance

/seL4-l4v-10.1.1/l4v/tools/autocorres/tests/examples/
H A Dplus.c15 unsigned int plus2(unsigned int a, unsigned int b) { function
24 return !(plus(1, 2) == plus2(1, 2));
/seL4-l4v-10.1.1/HOL4/help/src-sml/
H A DSymbolic.sml9 ("simpLib", "++", "plus2"),
20 | unsymb "simpLib.++" = "simpLib.plus2"
21 | unsymb "bossLib.++" = "bossLib.plus2"
32 | tosymb "simpLib.plus2" = "simpLib.++"
/seL4-l4v-10.1.1/HOL4/src/metis/
H A DmlibArbnum.sig17 val plus2 : num -> num value
H A DmlibArbnum.sml41 val plus2 = plus1 o plus1 value
/seL4-l4v-10.1.1/HOL4/src/quotient/Manual/
H A Dllncs.cls39 \abovedisplayshortskip \z@ \@plus2\p@
40 \belowdisplayshortskip 4\p@ \@plus2\p@ \@minus2\p@
43 \topsep 8\p@ \@plus2\p@ \@minus4\p@
322 \topsep 8\p@ \@plus2\p@ \@minus4\p@
329 \topsep 0\p@ \@plus2\p@ \@minus\p@}
864 \def\@spthm#1#2#3#4{\topsep 7\p@ \@plus2\p@ \@minus4\p@
889 \def\@Thm#1#2#3{\topsep 7\p@ \@plus2\p@ \@minus4\p@
/seL4-l4v-10.1.1/HOL4/src/emit/MLton/
H A DnumML.sml16 fun plus2 x = LargeInt.+(x, TWO) function
22 fun BIT2 n = plus2(times2 n)
/seL4-l4v-10.1.1/HOL4/src/portableML/mosml/
H A DArbnumcore.sig16 val plus2 : num -> num value
H A DArbnumcore.sml46 val plus2 = plus1 o plus1 value
/seL4-l4v-10.1.1/HOL4/src/portableML/poly/
H A DArbnumcore.sig16 val plus2 : num -> num value
H A DArbnumcore.sml26 fun plus2 x = x + 2 function
/seL4-l4v-10.1.1/HOL4/src/emit/
H A Dbasis_emitScript.sml282 \ | num2Arbnum (BIT2 n) = Arbnum.plus2(Arbnum.times2(num2Arbnum n))\n\

Completed in 57 milliseconds