The Coq mailing list

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

Thanks!  This is fascinating…  I feel like I am dealing with a very precise system J

 

From: coq-club-request AT inria.fr [mailto:coq-club-request AT inria.fr] On Behalf Of Cedric Auger
Sent: Tuesday, November 18, 2014 22:57
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] How do I enter a decimal 1.1 in COQ?

 

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\...