The Coq mailing list

[Victor Porton <porton AT narod.ru>]

09.11.2011, 03:58, "Alexandre Pilkiewicz" 
<alexandre.pilkiewicz AT polytechnique.org>:
> 2011/11/8 Victor Porton 
>Â <porton AT narod.ru>:
>
>> šBut how to make it to work as intended, that is how to deal with the 
>> projector "num" OF THE CURRENT INSTANCE INSIDE AN INSTANCE PROOF?
>
> IT HAS ALREADY BEEN REPLACED BY ITS DEFINITION, WHICH IS WHY YOU HAVE
> TO PROVE 0=0.
>
>> šInstance C2: C := { num:=0 }.
>> šproof.
>> ššhave (num=0) using tauto.
>> šend proof.
>
> num is a projector, that expects an instance of the class C as an
> argument, and you have not defined sur an instance yet. So your code
> still makes *no sense*

Maybe it makes no sense.

But how to use projectors in an instance proof?

Or if it's impossible to use projectors in an instance proof, what can be 
done instead?

What I ask, is some example of how to write instance proofs. Can it be done 
without using projectors?

-- 
Victor Porton - http://portonvictor.org