diff options
| author |  msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-11-17 10:34:57 +0000 |
|---|---|---|
| committer | msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-11-17 10:34:57 +0000 |
| commit | 1011266b84371b34536dd5aa5afb3a44b8f8d53c (patch) | |
| tree | d36b17a2127b1d9df2135b04f7b4f4e28f096615 /theories/Numbers/Natural | |
| parent | 6ffdff6e96aa52ca8512634c4bf1bba4252b91d6 (diff) | |
Merge subinstances branch by me and Tom Prince.
This adds two experimental features to the typeclass implementation:
- Path cuts: a way to specify through regular expressions on instance names
search pathes that should be avoided (e.g. [proper_flip proper_flip]).
Regular expression matching is implemented through naïve derivatives.
- Forward hints for subclasses: e.g. [Equivalence -> Reflexive] is no
longer applied backwards, but introducing a specific [Equivalence] in the
environment register a [Reflexive] hint as well. Currently not
backwards-compatible, the next patch will allow to specify direction
of subclasses hints.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14671 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Numbers/Natural')
| -rw-r--r-- | theories/Numbers/Natural/Abstract/NBits.v | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/theories/Numbers/Natural/Abstract/NBits.v b/theories/Numbers/Natural/Abstract/NBits.v index ce720c38c..c66f003ec 100644 --- a/theories/Numbers/Natural/Abstract/NBits.v +++ b/theories/Numbers/Natural/Abstract/NBits.v @@ -48,6 +48,9 @@ Qed. Definition b2n (b:bool) := if b then 1 else 0. Local Coercion b2n : bool >-> t. +Instance b2n_proper : Proper (Logic.eq ==> eq) b2n. +Proof. solve_proper. Qed. + Lemma exists_div2 a : exists a' (b:bool), a == 2*a' + b. Proof. elim (Even_or_Odd a); [intros (a',H)| intros (a',H)]. |