index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
test-suite
/
bugs
/
closed
/
bug_11421.v
blob: 8ddf05c8886b0a6a23ad115ef4f9ccd1ecdacae8 (
plain
)
1
Fail
Definition
plus1_plus1
:
Type
@{
Set
+
1
}
:=
Type
@{
Set
+
1
}.