blob: c3f2fb5b4240fba930e30782c9928c16ced64957 (
plain)
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
|
32%Z
: Z
eq_refl : 42%Z = 42%Z
: 42%Z = 42%Z
fun f : nat -> Z => (f 0%nat + 0)%Z
: (nat -> Z) -> Z
fun x : positive => Z.pos x~0
: positive -> Z
fun x : positive => (Z.pos x + 1)%Z
: positive -> Z
fun x : positive => Z.pos x
: positive -> Z
fun x : positive => Z.neg x~0
: positive -> Z
fun x : positive => (Z.pos x~0 + 0)%Z
: positive -> Z
fun x : positive => (- Z.pos x~0)%Z
: positive -> Z
fun x : positive => (- Z.pos x~0 + 0)%Z
: positive -> Z
(Z.of_nat 0 + 1)%Z
: Z
(0 + Z.of_nat (0 + 0))%Z
: Z
Z.of_nat 0 = 0%Z
: Prop
(0 + Z.of_nat 11)%Z
: Z
0x2a%Z
: Z
(-0x2a)%Z
: Z
0x0%Z
: Z
|
