coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Error: 1 * n = n.

From: soham chakraborty <soham4you AT gmail.com>
To: coq-club AT inria.fr
Subject: [Coq-Club] Error: 1 * n = n.
Date: Thu, 5 Sep 2013 13:04:45 +0530

Hi,
I am a Coq beginner. I am trying the following theorem on coqIde

Theorem mult_1_l : forall n:nat, 1 * n = n.
Proof.
intros n. reflexivity. Qed.

But having follwing error message while hitting the tactic reflexivity.
Error: Impossible to unify "n" with "1 * n".

Can you please explain the problem.

Thanks in advance.

Best Regards,
soham

[Coq-Club] Error: 1 * n = n., soham chakraborty, 09/05/2013
- Re: [Coq-Club] Error: 1 * n = n., Valentin Robert, 09/05/2013
  - Re: [Coq-Club] Error: 1 * n = n., soham chakraborty, 09/05/2013
    - RE: [Coq-Club] Error: 1 * n = n., Nick Benton, 09/05/2013
      - Re: [Coq-Club] Error: 1 * n = n., Colm Bhandal, 09/05/2013
        
        Re: [Coq-Club] Error: 1 * n = n., Valentin Robert, 09/05/2013
        
        Re: [Coq-Club] Error: 1 * n = n., Colm Bhandal, 09/05/2013
        
        Re: [Coq-Club] Error: 1 * n = n., Kristopher Micinski, 09/05/2013
        Message not available
        Re: [Coq-Club] Error: 1 * n = n., Kristopher Micinski, 09/05/2013
        Re: [Coq-Club] Error: 1 * n = n., soham chakraborty, 09/05/2013
        Re: [Coq-Club] Error: 1 * n = n., t x, 09/05/2013