diff options
| author | Arnaud Spiwack | 2014-09-26 14:53:38 +0200 |
|---|---|---|
| committer | Arnaud Spiwack | 2014-09-26 14:55:09 +0200 |
| commit | c74a70a73b3bf39394c551f1cdb224450bf77176 (patch) | |
| tree | a120c278e096116cb4384904169c882dc0f26201 /kernel/nativecode.ml | |
| parent | 48ba4c55159d0d9f9b13cfe82617ac4a68867885 (diff) | |
Hurkens.v: new paradox: type of modal propositions is not a retract.
In particular there is no retract of the type of negative propositions in a negative proposition.
Diffstat (limited to 'kernel/nativecode.ml')
0 files changed, 0 insertions, 0 deletions