The Coq mailing list

["Soegtrop, Michael" <michael.soegtrop AT intel.com>]

Dear Nikhil,

 

adding to what Benoit and David wrote: the conversion between 0 and O, 1 and S O and so on is an integrated notational transformation done by Coq. Essentially when reading 1 Coq will convert it to S O and when writing S O it will convert it to 1 (unless you have printing notation switched off). As far as I know this is “hard wired” and you cannot define such transformations yourself. Also this notation only works for various types of numbers defined in Coq libraries. It won’t work for numbers you define on your own (you can define coercions, though).

 

Best regards,

 

Michael

 

From: coq-club-request AT inria.fr [mailto:coq-club-request AT inria.fr] On Behalf Of nikhil kaushik
Sent: Wednesday, May 24, 2017 6:51 AM
To: coq-club AT inria.fr
Subject: [Coq-Club] Question while learning Coq from Software Foundations book

 

I was going through the book Software foundations to learn Coq and I got stuck on Numbers. In this Type definition

Inductive nat : Type :=

  | O : nat

  | S : nat -> nat.

How does O becomes 0 when we use it in definition of

Definition pred (n : nat) : nat :=

  match n with

    | O => O

    | S n' => n'

  end.

I only understood that O represents natural numbers and S takes a natural number and return another natural number so S is a function. What I do not get is when our defined nat data type is used in preddefinition how does O represent 0? And how does S n' pattern match gives us predecessor of n.

 

--

~Nikhil Kaushik

Intel Deutschland GmbH
Registered Address: Am Campeon 10-12, 85579 Neubiberg, Germany
Tel: +49 89 99 8853-0, www.intel.de
Managing Directors: Christin Eisenschmid, Christian Lamprechter
Chairperson of the Supervisory Board: Nicole Lau
Registered Office: Munich
Commercial Register: Amtsgericht Muenchen HRB 186928