diff options
| author | Anton Trunov | 2020-05-12 18:29:28 +0300 |
|---|---|---|
| committer | Anton Trunov | 2020-05-12 18:29:28 +0300 |
| commit | 5784bb98aaa3e4eab4cd3e9871afb4b40d82f62c (patch) | |
| tree | bbe30c8c8aaffbd387e886bae4c017db9c525b90 /theories/Sets | |
| parent | efb78e3c413bcc66d470ba4046c56bae0a61f56f (diff) | |
| parent | 1019cb48c80260d7df27096826e8594ec242dc5a (diff) | |
Merge PR #12162: Fixing #12161: rename Bool.leb into Bool.le
Ack-by: Zimmi48
Reviewed-by: anton-trunov
Diffstat (limited to 'theories/Sets')
| -rw-r--r-- | theories/Sets/Uniset.v | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/theories/Sets/Uniset.v b/theories/Sets/Uniset.v index 31e8cf463e..474b417e8e 100644 --- a/theories/Sets/Uniset.v +++ b/theories/Sets/Uniset.v @@ -44,18 +44,18 @@ Definition In (s:uniset) (a:A) : Prop := charac s a = true. Hint Unfold In : core. (** uniset inclusion *) -Definition incl (s1 s2:uniset) := forall a:A, leb (charac s1 a) (charac s2 a). +Definition incl (s1 s2:uniset) := forall a:A, Bool.le (charac s1 a) (charac s2 a). Hint Unfold incl : core. (** uniset equality *) Definition seq (s1 s2:uniset) := forall a:A, charac s1 a = charac s2 a. Hint Unfold seq : core. -Lemma leb_refl : forall b:bool, leb b b. +Lemma le_refl : forall b, Bool.le b b. Proof. destruct b; simpl; auto. Qed. -Hint Resolve leb_refl : core. +Hint Resolve le_refl : core. Lemma incl_left : forall s1 s2:uniset, seq s1 s2 -> incl s1 s2. Proof. |