The Coq mailing list

[Antonia Balaa <Antonia.Balaa AT sophia.inria.fr>]

Dear all,

        I'm trying to type the expressions: titi and toto (see below),
 and I would like to know why these two terms do not have the same type.
The last Check command raises an error. Could you explain me why?

Best Regards.
        Antonia
-----------------------------------------------------------------------------

Require Arith.
Require Compare_dec.

Variable x : nat.
Variable toto :  O
        =(<[_:{x=O}+{(lt O x)}]nat>Cases (zerop x) of
            (left _) => O
          | (right _) => O
          end).

Variable titi : O = (Cases (zerop x) of
                       (left _) => O
                     | (right _) => O
                     end).

Check (titi::  O
        =(<[_:{x=O}+{(lt O x)}]nat>Cases (zerop x) of
            (left _) => O
          | (right _) => O
          end)).


  Antonia