forked from digama0/lean4checker
-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathbitvec_functions.tex
19 lines (19 loc) · 3.38 KB
/
bitvec_functions.tex
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
\hspace{-2em}\begin{tabular}{|l|C|C|C|C|C|C|C|C|C|C|C|C|C|C|C|C|C|C|C|C|C|C|C|C|C|C|C|C|C|C|C|C|}
\hline
& \tablerotate{add} & \tablerotate{sub} & \tablerotate{neg} & \tablerotate{abs} & \tablerotate{mul} & \tablerotate{udiv} & \tablerotate{umod} & \tablerotate{sdiv} & \tablerotate{srem} & \tablerotate{smod} & \tablerotate{ofBool} & \tablerotate{fill} & \tablerotate{extract} & \tablerotate{extractLsb'} & \tablerotate{setWidth} & \tablerotate{shiftLeftZeroExtend} & \tablerotate{setWidth'} & \tablerotate{signExtend} & \tablerotate{and} & \tablerotate{or} & \tablerotate{xor} & \tablerotate{not} & \tablerotate{shiftLeft} & \tablerotate{ushiftRight} & \tablerotate{sshiftRight} & \tablerotate{sshiftRight'} & \tablerotate{rotateLeft} & \tablerotate{rotateRight} & \tablerotate{append} & \tablerotate{replicate} & \tablerotate{concat} & \tablerotate{twoPow} \\
\hline
toNat & \tableok & \tableok & \tableok & \tableok & \tableok & \tableok & \tableok & \tableok & \tableno & \tableok & \tableok & \tableok & \tableok & \tableok & \tableok & \tableno & \tableok & \tableok & \tableok & \tableok & \tableok & \tableok & \tableok & \tableok & \tableno & \tableno & \tableno & \tableno & \tableok & \tableno & \tableok & \tableok \\
\hline
toInt & \tableok & \tableok & \tableok & \tableok & \tableok & \tableno & \tableno & \tableno & \tableno & \tableno & \tableok & \tableok & \tableno & \tableno & \tableok & \tableno & \tableno & \tableok & \tableok & \tableok & \tableok & \tableok & \tableok & \tableok & \tableno & \tableno & \tableno & \tableno & \tableno & \tableno & \tableok & \tableno \\
\hline
toFin & \tableok & \tableok & \tableok & \tableno & \tableok & \tableno & \tableno & \tableno & \tableno & \tableno & \tableok & \tableok & \tableno & \tableno & \tableok & \tableno & \tableno & \tableno & \tableok & \tableok & \tableok & \tableok & \tableok & \tableno & \tableno & \tableno & \tableno & \tableno & \tableno & \tableno & \tableok & \tableno \\
\hline
getElem & \tableok & \tableok & \tableok & \tableok & \tableok & \tableno & \tableno & \tableno & \tableno & \tableno & \tableok & \tableok & \tableok & \tableok & \tableok & \tableok & \tableok & \tableok & \tableok & \tableok & \tableok & \tableok & \tableok & \tableok & \tableok & \tableok & \tableok & \tableok & \tableok & \tableok & \tableok & \tableok \\
\hline
getLsbD & \tableok & \tableok & \tableok & \tableok & \tableok & \tableno & \tableno & \tableno & \tableno & \tableno & \tableok & \tableok & \tableok & \tableok & \tableok & \tableok & \tableok & \tableok & \tableok & \tableok & \tableok & \tableok & \tableok & \tableok & \tableok & \tableok & \tableok & \tableok & \tableok & \tableok & \tableok & \tableok \\
\hline
getMsbD & \tableok & \tableok & \tableok & \tableok & \tableno & \tableno & \tableno & \tableno & \tableno & \tableno & \tableok & \tableok & \tableno & \tableno & \tableok & \tableok & \tableok & \tableok & \tableok & \tableok & \tableok & \tableok & \tableok & \tableok & \tableok & \tableok & \tableok & \tableok & \tableok & \tableno & \tableok & \tableok \\
\hline
msb & \tableok & \tableok & \tableok & \tableok & \tableok & \tableno & \tableno & \tableno & \tableno & \tableno & \tableok & \tableok & \tableno & \tableno & \tableok & \tableok & \tableok & \tableok & \tableok & \tableok & \tableok & \tableok & \tableok & \tableok & \tableok & \tableok & \tableok & \tableok & \tableok & \tableno & \tableok & \tableok \\
\hline
\end{tabular}