path: root/cheri/sail_latexcc/sailccHighestSetBit.tex

val HighestSetBit : forall 'N , 'N >= 2. #\hyperref[zbits]{bits}#('N) -> {'n, 0 <= 'n < 'N . (bool, atom('n))}