| Mode | Name | Size | |
|---|---|---|---|
| -rw-r--r-- | absterm.art | 108 | logplain |
| -rw-r--r-- | absthm.art | 95 | logplain |
| -rw-r--r-- | appterm.art | 146 | logplain |
| -rw-r--r-- | appthm.art | 155 | logplain |
| -rw-r--r-- | assume.art | 55 | logplain |
| -rw-r--r-- | axiom.art | 58 | logplain |
| -rw-r--r-- | betaconv.art | 119 | logplain |
| -rw-r--r-- | cons.art | 23 | logplain |
| -rw-r--r-- | const.art | 13 | logplain |
| -rw-r--r-- | constterm.art | 48 | logplain |
| -rw-r--r-- | deductantisym.art | 81 | logplain |
| -rw-r--r-- | def.art | 31 | logplain |
| -rw-r--r-- | defineconst.art | 61 | logplain |
| -rw-r--r-- | definetypeop.art | 173 | logplain |
| -rw-r--r-- | eqmp.art | 187 | logplain |
| -rw-r--r-- | name.art | 7 | logplain |
| -rw-r--r-- | name2.art | 5 | logplain |
| -rw-r--r-- | nil.art | 4 | logplain |
| -rw-r--r-- | null.art | 0 | logplain |
| -rw-r--r-- | number.art | 3 | logplain |
| -rw-r--r-- | opType.art | 25 | logplain |
| -rw-r--r-- | pop.art | 8 | logplain |
| -rw-r--r-- | ref.art | 37 | logplain |
| -rw-r--r-- | refl.art | 39 | logplain |
| -rw-r--r-- | remove.art | 40 | logplain |
| -rw-r--r-- | subst.art | 273 | logplain |
| -rw-r--r-- | thm.art | 114 | logplain |
| -rw-r--r-- | timer.sh | 57 | logplain |
| -rw-r--r-- | typeop.art | 14 | logplain |
| -rw-r--r-- | var.art | 26 | logplain |
| -rw-r--r-- | varterm.art | 34 | logplain |
| -rw-r--r-- | vartype.art | 15 | logplain |
 |
index : opentheory-transform | |
| Opentheory proof trace optimizer | Jed Barber |
| summaryrefslogtreecommitdiff |