| Mode | Name | Size | |
|---|---|---|---|
| -rw-r--r-- | ConstructiveAbs.v | 12280 | logplain |
| -rw-r--r-- | ConstructiveLUB.v | 18696 | logplain |
| -rw-r--r-- | ConstructiveLimits.v | 18381 | logplain |
| -rw-r--r-- | ConstructiveMinMax.v | 25610 | logplain |
| -rw-r--r-- | ConstructivePower.v | 9728 | logplain |
| -rw-r--r-- | ConstructiveReals.v | 40558 | logplain |
| -rw-r--r-- | ConstructiveRealsMorphisms.v | 50055 | logplain |
| -rw-r--r-- | ConstructiveSum.v | 23208 | logplain |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |