| Mode | Name | Size | |
|---|---|---|---|
| -rw-r--r-- | ConstructiveAbs.v | 36065 | logplain |
| -rw-r--r-- | ConstructiveLUB.v | 18616 | logplain |
| -rw-r--r-- | ConstructiveLimits.v | 36943 | logplain |
| -rw-r--r-- | ConstructiveReals.v | 40486 | logplain |
| -rw-r--r-- | ConstructiveRealsMorphisms.v | 52221 | logplain |
| -rw-r--r-- | ConstructiveSum.v | 12598 | logplain |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |