coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] what does "Bound to class nat" mean?

From: Matej Košík <mail AT matej-kosik.net>
To: Coq Club <coq-club AT inria.fr>
Subject: [Coq-Club] what does "Bound to class nat" mean?
Date: Sun, 12 Nov 2017 14:09:09 +0100
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=mail AT matej-kosik.net; spf=SoftFail smtp.mailfrom=mail AT matej-kosik.net; spf=SoftFail smtp.helo=postmaster AT matej-kosik.net
Ironport-phdr: 9a23:CbzCgx+/cdrvyP9uRHKM819IXTAuvvDOBiVQ1KB90+IcTK2v8tzYMVDF4r011RmSAtWdtqoMotGVmp6jcFRI2YyGvnEGfc4EfD4+ouJSoTYdBtWYA1bwNv/gYn9yNs1DUFh44yPzahANS47WLmffqXyq7DMUBg63dU8sfry0SaPMgt6I1+Gu9tiWSk0IwWPlOfIhZCmx+C7Wr4E9hZZoYvI6zQKMqX9VccxXw3lpLBSdhUCvyN23+ctG+jhduboC8DzFUu2ueq05SZRdBSgrMSU249bqtl/FQBfZtShUaXkfjhcdW1uN1xr9RJqk93Gi7uc=
Openpgp: id=1CD41D0A52319DC7ABC1B79F50AFFA128CE48649; url=http://matej-kosik.net/doc/kosik.asc

Hi,

When I type, e.g.:

Print Scope nat_scope.

I see:

Scope nat_scope
Delimiting key is nat
Bound to class nat
"x >= y" := ge x y
"x > y" := gt x y
"x <= y <= z" := and (le x y) (le y z)
"x <= y < z" := and (le x y) (lt y z)
"n <= m" := le n m
"x < y <= z" := and (lt x y) (le y z)
"x < y < z" := and (lt x y) (lt y z)
"x < y" := lt x y
"x - y" := Nat.sub x y
"x + y" := Nat.add x y
"x * y" := Nat.mul x y

Everything is clear, except for:

Bound to class nat

clause. What does that mean? Does anybody know? What si "nat class"?

Attachment: signature.asc
Description: OpenPGP digital signature

[Coq-Club] what does "Bound to class nat" mean?, Matej Košík, 11/12/2017
- Re: [Coq-Club] what does "Bound to class nat" mean?, Ralf Jung, 11/12/2017
  - Re: [Coq-Club] what does "Bound to class nat" mean?, Hugo Herbelin, 11/15/2017