Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] what does "Bound to class nat" mean?

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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


Chronological Thread 
  • From: Ralf Jung <jung AT mpi-sws.org>
  • To: coq-club AT inria.fr, Matej Košík <mail AT matej-kosik.net>
  • Subject: Re: [Coq-Club] what does "Bound to class nat" mean?
  • Date: Sun, 12 Nov 2017 22:05:47 +0100
  • Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=jung AT mpi-sws.org; spf=Pass smtp.mailfrom=jung AT mpi-sws.org; spf=None smtp.helo=postmaster AT jupiter.mpi-klsb.mpg.de
  • Ironport-phdr: 9a23:kGCh/RG3L432u83r1O52DJ1GYnF86YWxBRYc798ds5kLTJ76r8mwAkXT6L1XgUPTWs2DsrQf1LqQ7viocFdDyKjCmUhKSIZLWR4BhJdetC0bK+nBN3fGKuX3ZTcxBsVIWQwt1Xi6NU9IBJS2PAWK8TXhpQIVTx74LE9+Ivn/Mo/UlcW+ke6ov9X2ahlFhnKeZkH3L13iqAzQsuETiJdvKOMyzQDIoT1OdvgAlk1yIlfGpR/46I+S4Zhsu3BSpvQu38tYUODhYL9+SqZXWmd1e1sp7dHm4EGQBTCE4WERBz0b

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"?

I assume this is the result of a `Bind Scope nat_scope with nat`, which
essentially means that nat_scope is used automatically for parsing
arguments of a function of type nat -> ....

Why this is called a "class", I have no idea.

Kind regards,
Ralf



Archive powered by MHonArc 2.6.18.

Top of Page