From f9312f45b386c33723c0ec7741556e9389639f2c Mon Sep 17 00:00:00 2001 From: Kazuhiko Sakaguchi Date: Wed, 30 Oct 2019 15:41:58 +0100 Subject: 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. --- doc/changelog/04-tactics/10998-zify-complements.rst | 7 +++++++ 1 file changed, 7 insertions(+) create mode 100644 doc/changelog/04-tactics/10998-zify-complements.rst (limited to 'doc') diff --git a/doc/changelog/04-tactics/10998-zify-complements.rst b/doc/changelog/04-tactics/10998-zify-complements.rst new file mode 100644 index 0000000000..e0632e3f74 --- /dev/null +++ b/doc/changelog/04-tactics/10998-zify-complements.rst @@ -0,0 +1,7 @@ +- The :tacn:`zify` tactic is now aware of `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`, and `Z.quot2`. + Injections for internal definitions in `ZifyBool.v` (`isZero` and `isLeZero`) + are also added to help users to declare new :tacn:`zify` class instances using + Micromega tactics. + (`#10998 `_, by Kazuhiko Sakaguchi). -- cgit v1.2.3