summaryrefslogtreecommitdiff
path: root/test-suite/output/ZSyntax.out
blob: f23198b0f3f8cff42fdd1563f8f2642e9756104f (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
32%Z
     : Z
fun f : nat -> Z => (f 0%nat + 0)%Z
     : (nat -> Z) -> Z
fun x : positive => Zpos x~0
     : positive -> Z
fun x : positive => (Zpos x + 1)%Z
     : positive -> Z
fun x : positive => Zpos x
     : positive -> Z
fun x : positive => Zneg x~0
     : positive -> Z
fun x : positive => (Zpos x~0 + 0)%Z
     : positive -> Z
fun x : positive => (- Zpos x~0)%Z
     : positive -> Z
fun x : positive => (- Zpos 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