index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
test-suite
/
output
/
InitSyntax.v
blob: 90fad3718fc696007fba3acfd4d45b4f3216a0c1 (
plain
)
1
2
3
4
(
*
Soumis
par
Pierre
*
)
Print
sig2
.
Check
(
EX
x:
nat
|
x
=
x
).
Check
[
b:
bool
]
if
b
then
b
else
b
.