]>
-rw-r--r-- | 223 | Makefile | blob | raw |
drwxr-xr-x | - | TPTP | tree |
-rw-r--r-- | 1278 | absurd.ma | blob | raw |
-rw-r--r-- | 2098 | apply.ma | blob | raw |
-rw-r--r-- | 1174 | apply2.ma | blob | raw |
-rw-r--r-- | 1542 | applys.ma | blob | raw |
-rw-r--r-- | 1538 | assumption.ma | blob | raw |
-rw-r--r-- | 1282 | bad_induction.ma | blob | raw |
drwxr-xr-x | - | bad_tests | tree |
-rw-r--r-- | 22911 | bool.ma | blob | raw |
-rw-r--r-- | 1695 | change.ma | blob | raw |
-rw-r--r-- | 1307 | clear.ma | blob | raw |
-rw-r--r-- | 1362 | clearbody.ma | blob | raw |
-rw-r--r-- | 4295 | coercions.ma | blob | raw |
-rw-r--r-- | 1725 | coercions_contravariant.ma | blob | raw |
-rw-r--r-- | 1488 | coercions_dependent.ma | blob | raw |
-rw-r--r-- | 1811 | coercions_nonuniform.ma | blob | raw |
-rw-r--r-- | 1587 | coercions_open.ma | blob | raw |
-rw-r--r-- | 4046 | coercions_propagation.ma | blob | raw |
-rw-r--r-- | 5768 | coercions_russell.ma | blob | raw |
-rw-r--r-- | 1380 | color.ma | blob | raw |
-rw-r--r-- | 1389 | comments.ma | blob | raw |
-rw-r--r-- | 1718 | compose.ma | blob | raw |
-rw-r--r-- | 1171 | constructor.ma | blob | raw |
-rw-r--r-- | 2246 | continuationals.ma | blob | raw |
-rw-r--r-- | 1348 | contradiction.ma | blob | raw |
-rw-r--r-- | 1202 | cut.ma | blob | raw |
-rw-r--r-- | 6606 | decl.ma | blob | raw |
-rw-r--r-- | 1344 | decompose.ma | blob | raw |
-rw-r--r-- | 1952 | demodulation_coq.ma | blob | raw |
-rw-r--r-- | 1400 | demodulation_matita.ma | blob | raw |
-rw-r--r-- | 1795 | dependent_guarded_bove_capretta.ma | blob | raw |
-rw-r--r-- | 2069 | dependent_injection.ma | blob | raw |
-rw-r--r-- | 1091 | dependent_type_inference.ma | blob | raw |
-rw-r--r-- | 13652 | depends | blob | raw |
-rw-r--r-- | 3001 | destruct.ma | blob | raw |
-rw-r--r-- | 1317 | diabolic_fix.ma | blob | raw |
-rw-r--r-- | 2901 | elim.ma | blob | raw |
-rw-r--r-- | 1242 | elim_pattern.ma | blob | raw |
-rw-r--r-- | 2656 | fguidi.ma | blob | raw |
-rw-r--r-- | 1457 | first.ma | blob | raw |
-rw-r--r-- | 1371 | fix_betareduction.ma | blob | raw |
-rw-r--r-- | 1289 | fix_che_non_passa_ma_dovrebbe.ma | blob | raw |
-rw-r--r-- | 1399 | fold.ma | blob | raw |
-rwxr-xr-x | 1831 | formal_topology.ma | blob | raw |
-rw-r--r-- | 1790 | generalize.ma | blob | raw |
-rw-r--r-- | 27468 | hard_refine.ma | blob | raw |
-rw-r--r-- | 2084 | injection.ma | blob | raw |
drwxr-xr-x | - | interactive | tree |
-rw-r--r-- | 2088 | inversion.ma | blob | raw |
-rw-r--r-- | 1919 | inversion2.ma | blob | raw |
-rw-r--r-- | 1298 | letrec.ma | blob | raw |
-rw-r--r-- | 1827 | letrecand.ma | blob | raw |
-rw-r--r-- | 2824 | luo.ma | blob | raw |
-rw-r--r-- | 1859 | match_inference.ma | blob | raw |
-rw-r--r-- | 4174 | metasenv_ordering.ma | blob | raw |
-rw-r--r-- | 1961 | multiple_inheritance.ma | blob | raw |
-rw-r--r-- | 1054 | mysql_escaping.ma | blob | raw |
-rw-r--r-- | 1734 | naiveparamod.ma | blob | raw |
-rw-r--r-- | 1338 | overred.ma | blob | raw |
-rw-r--r-- | 1532 | paramodulation.ma | blob | raw |
drwxr-xr-x | - | paramodulation | tree |
-rw-r--r-- | 2520 | pullback.ma | blob | raw |
-rw-r--r-- | 1685 | record.ma | blob | raw |
-rw-r--r-- | 1861 | replace.ma | blob | raw |
-rw-r--r-- | 2588 | rewrite.ma | blob | raw |
-rw-r--r-- | 50 | root | blob | raw |
-rw-r--r-- | 1320 | second.ma | blob | raw |
-rw-r--r-- | 1945 | simpl.ma | blob | raw |
-rw-r--r-- | 1947 | tacticals.ma | blob | raw |
-rw-r--r-- | 1288 | test2.ma | blob | raw |
-rw-r--r-- | 1385 | test3.ma | blob | raw |
-rw-r--r-- | 1429 | test4.ma | blob | raw |
-rw-r--r-- | 1327 | third.ma | blob | raw |
-rw-r--r-- | 1590 | tinycals.ma | blob | raw |
-rw-r--r-- | 1710 | unfold.ma | blob | raw |