File: RealNumberSyntax.out

package info (click to toggle)
coq 8.20.1%2Bdfsg-1
  • links: PTS, VCS
  • area: main
  • in suites: sid, trixie
  • size: 44,116 kB
  • sloc: ml: 234,160; sh: 4,301; python: 3,270; ansic: 2,644; makefile: 882; lisp: 172; javascript: 63; xml: 24; sed: 2
file content (84 lines) | stat: -rw-r--r-- 861 bytes parent folder | download | duplicates (4)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
32%R
     : R
(-31)%R
     : R
1.5%R
     : R
1.5e1%R
     : R
eq_refl : 1.02 = 102e-2
     : 1.02 = 102e-2
1.02e1
     : R
102e-1
     : R
1.02e3
     : R
102e1
     : R
1.02e2
     : R
102
     : R
10.2e-1
     : R
1.02
     : R
eq_refl : -0.0001 = -1e-4
     : -0.0001 = -1e-4
eq_refl : -0.50 = -50e-2
     : -0.50 = -50e-2
eq_refl : -26 = -26
     : -26 = -26
eq_refl : 0xb.2c%xR = 0xb2cp-8%xR
     : 0xb.2c%xR = 0xb2cp-8%xR
eq_refl : -6882 = -6882
     : -6882 = -6882
0xb.2cp2%xR
     : R
0xb2cp-6%xR
     : R
0xb.2cp8%xR
     : R
2860
     : R
(-0xb.2cp-2)%xR
     : R
- 0xb2cp-10%xR
     : R
0
     : R
0
     : R
42
     : R
42
     : R
1.23
     : R
0x1.23%xR
     : R
0.0012
     : R
42e3
     : R
42e-3
     : R
0x0
     : R
0x0
     : R
0x2a
     : R
0x2a
     : R
1.23%R
     : R
0x1.23
     : R
0x0.0012
     : R
0x2ap3
     : R
0x2ap-3
     : R