The Coq mailing list

[Cedric Auger <sedrikov AT gmail.com>]

Try to divide 11 by 10. I guess something like (11/10)%R should work.

2014-11-18 14:50 GMT+01:00 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

--

.../Sedrikov\...