The Coq mailing list

[Lionel Elie Mamane <lionel AT mamane.lu>]

Hi,

Does Coq permit me to do pattern matching on a type while defining
this same type?

What I'm trying to do (with version 7.2) is something like:

Inductive Example : Type :=
   Example1: nat -> Example
 | Example2:
  let check = [e:Example]
    Cases e of
     (Example1 n) => (lt (S (S O)) n)
    |(Example2 e p) => false
    end
  in
 (e:Example) (check e)-> Example.


In the definition of check, Coq complains is not a constructor, while
it should:

Error: The symbol Example1 should be a constructor


Well... It is a constructor of the type I'm currently defining.

So is there a way around this?

Thank you for your help,

-- 
Lionel

Attachment: pgpsF1gBOQr0I.pgp
Description: PGP signature