diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-11-10 11:19:21 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-11-10 11:19:21 +0000 |
| commit | 424b20ed34966506cef31abf85e3e3911138f0fc (patch) | |
| tree | 6239f8c02d629b5ccff23213dc1ff96dd040688b /theories/QArith | |
| parent | e03541b7092e136edc78335cb178c0217dd48bc5 (diff) | |
DecidableType: A specification via boolean equality as an alternative to eq_dec
+ adaptation of {Nat,N,P,Z,Q,R}_as_DT for them to provide both eq_dec and eqb
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12488 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/QArith')
| -rw-r--r-- | theories/QArith/QOrderedType.v | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/theories/QArith/QOrderedType.v b/theories/QArith/QOrderedType.v index f6f457f65..f383491d9 100644 --- a/theories/QArith/QOrderedType.v +++ b/theories/QArith/QOrderedType.v @@ -20,10 +20,14 @@ Module Q_as_DT <: DecidableType. Definition eq_dec := Qeq_dec. (** The next fields are not mandatory, but allow [Q_as_DT] to be - also a [DecidableTypeOrig]. *) + also a [DecidableTypeOrig] (resp. a [BooleanEqualityType]). *) Definition eq_refl := Qeq_refl. Definition eq_sym := Qeq_sym. Definition eq_trans := eq_trans. + + Definition eqb := Qeq_bool. + Definition eqb_eq := Qeq_bool_iff. + End Q_as_DT. |