diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-01-20 11:53:58 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-01-20 11:53:58 +0000 |
| commit | ddcbe6e926666cdc4bd5cd4a88d637efc338290c (patch) | |
| tree | 75ebb40b14683b18bf454eed439deb60ef171d7b /kernel/univ.ml | |
| parent | c7c3fd68b065bcdee45585b2241c91360223b249 (diff) | |
Numbers: simplier spec for testbit
We now specify testbit by some initial and recursive equations.
The previous spec (via a complex split of the number in
low and high parts) is now a derived property in {N,Z}Bits.v
This way, proofs of implementations are quite simplier.
Note that these new specs doesn't imply anymore that testbit is a
morphism, we have to add this as a extra spec (but this lead
to trivial proofs when implementing).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13792 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel/univ.ml')
0 files changed, 0 insertions, 0 deletions