index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
test-suite
/
output
/
ZSyntax.v
blob: 0f5092c416b0a548a1034dba7578bbf1fc445870 (
plain
)
1
2
3
Require
ZArith
.
Check
`
32
`
.
Check
[
f:
nat
->
Z
]
`
(
f
O
)
+
0
`
.
