aboutsummaryrefslogtreecommitdiff
path: root/kernel/cbytecodes.mli
diff options
context:
space:
mode:
authorKazuhiko Sakaguchi2019-10-30 15:41:58 +0100
committerKazuhiko Sakaguchi2019-11-15 14:20:21 +0900
commitf9312f45b386c33723c0ec7741556e9389639f2c (patch)
tree9101b25d03f72ac10ea1cc0d015c13b86895a455 /kernel/cbytecodes.mli
parent3d5d194742162255420907101c515aa26c237d25 (diff)
Add missing zify class instances
Add missing zify class instances for `Pos.pred_double`, `Pos.pred_N`, `Pos.of_nat`, `Pos.add_carry`, `Pos.pow`, `Pos.square`, `Z.pow`, `Z.double`, `Z.pred_double`, `Z.succ_double`, `Z.square`, `Z.div2`, `Z.quot2`, `isZero`, and `isLeZero`. Instances for `isZero` and `isLeZero` are useful to provide new zify instances by using Micromega tactics.
Diffstat (limited to 'kernel/cbytecodes.mli')
0 files changed, 0 insertions, 0 deletions