| Mode | Name | Size | |
|---|---|---|---|
| -rw-r--r-- | assumptions.rst | 7694 | logplain |
| -rw-r--r-- | basic.rst | 20615 | logplain |
| -rw-r--r-- | coinductive.rst | 7741 | logplain |
| -rw-r--r-- | conversion.rst | 10093 | logplain |
| -rw-r--r-- | definitions.rst | 8867 | logplain |
| -rw-r--r-- | index.rst | 1821 | logplain |
| -rw-r--r-- | inductive.rst | 63746 | logplain |
| -rw-r--r-- | modules.rst | 35229 | logplain |
| -rw-r--r-- | primitive.rst | 7399 | logplain |
| -rw-r--r-- | records.rst | 13096 | logplain |
| -rw-r--r-- | sections.rst | 4051 | logplain |
| -rw-r--r-- | sorts.rst | 4224 | logplain |
| -rw-r--r-- | variants.rst | 8445 | logplain |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |