The Coq mailing list

[Vladimir Voevodsky <vladimir AT ias.edu>]

Ok. Here is less complex code:

Inductive un : Type :=  . 

Definition nonsense ( x : un ) := match x with y => 0 end . 

Is this supposed to make sense? 

If so then what is "y" in the term "match x with y => 0 end "? Is it a 
variable? Is it a free variable or a bound variable? 

PS ... and if I write this:

Definition nonsense ( x : un ) := match x with y + 2 => 0 end . 

I get this:

> Toplevel input, characters 20-83:
> Anomaly: Uncaught exception Not_found(_). Please report.


(I am running trunk).






On Aug 3, 2014, at 8:12 PM, Michel Levy 
<michel.levy1948 AT gmail.com>
 wrote:

> On 03/08/2014 13:44, Cédric wrote:
>> Le Sun, 03 Aug 2014 13:17:26 +0200, Matej Kosik
>> <5764c029b688c1c0d24a2e97cd764f AT gmail.com>
>>  a écrit:
>> 
>>> Hi,
>>> 
>>> I would like to ask why if I introduce this definition:
>>> 
>>>  (* CoqArt, Section 6.1.1 (pg 138) *)
>>> 
>>>  Inductive month : Set :=
>>>  | January : month   | February : month | March : month    | April :
>>> month
>>>  | May : month       | June : month     | July : month     | August
>>> : month
>>>  | September : month | October : month  | November : month |
>>> December : month.
>>> 
>>> and then I try to define a function in the following way:
>>> 
>>>  (* Exercise 6.5 (pg 144) *)
>>> 
>>>  Definition month_has_even_number_of_days'' (leap:bool) (m:month) :=
>>>    match m with
>>>    | January | March | May | July | August | October | December =>
>>> false
>>>    | Feburary => negb leap
>>>    | April | June | September | November => true
>>>    end.
>>> 
>>> then I am getting a complaint:
>>> 
>>>  Toplevel input, characters 227-270:
>>>>  | April | June | September | November => true
>>>>    ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
>>> 
>>> Despite me tring to do fairly simple thing, the output thoroughly
>>> surprised me.
>>> Is the above response plausible? Why?
>> 
>> Probably because you mistyped "February" in "Feburary", thus
>> "Feburary" is considered as a variable matching all other cases. Then
>> April, June, September and November are considered already treated by
>> "Feburary"
>> 
>>> 
>>> A complementary question: why does Coq admit this:
>>> 
>>>  Definition month_with_even_number_of_days''' (leap:bool) (m:month) :=
>>>    match m with
>>>    | January | March | May | July | August | October | December =>
>>> false
>>>    | Feburary => negb leap
>>>    end.
>>> 
>>> instead of rejecting it due to cases that are not covered?
>> 
>> Because you continue to mistype February, and it is considered a
>> variable matching all other cases.
>> 
>> 
> I confirm the diagnostic of Cédric : Feburary is a variable matching all
> other cases.
> A good way to verify this is to print the  definition of
> month_with_even_number_of_days''' with
> Print month_with_even_number_of_days'''.
> 
> -- 
> email : 
> michel.levy1948 AT gmail.com
> http://membres-liglab.imag.fr/michel.levy 
>

Attachment: signature.asc
Description: Message signed with OpenPGP using GPGMail