The Coq mailing list

["Yasuaki Kudo" <yasu AT yasuaki.com>]

Hi,

 

I have just started to learn COQ and have no one to ask questions….  How do I enter a decimal 1.1 in COQ?  I think I figured out a way to enter 1%R but when I naively try 1.1%R, I get following errors.

 

 

Coq < Require Import Reals.

 

Coq < Check 1%R.       (This works)

1%R

     : R

 

Coq < Check 1.1%R.   (This doesn’t)

1

     : nat

 

Toplevel input, characters 9-10:

> Check 1.1%R.

>          ^

Syntax error: '.' or '...' expected after [tactic:tactic] (in [subgoal_command]).

 

Coq < Check (1.1)%R.    (This doesn’t, either)

Toplevel input, characters 8-9:

> Check (1.

>         ^

Syntax error: ',' or ')' expected after [constr:operconstr level 200] (in [constr:operconstr]).

 

Toplevel input, characters 10-11:

> Check (1.1)%R.

>           ^

Syntax error: '.' or '...' expected after [tactic:tactic] (in [subgoal_command]).

 

 

 

Cheers,

Yasu

Tokyo