]>
drwxr-xr-x | - | TPTP | tree |
-rw-r--r-- | 1330 | absurd.ma | blob | raw |
-rw-r--r-- | 2149 | apply.ma | blob | raw |
-rw-r--r-- | 1215 | apply2.ma | blob | raw |
-rw-r--r-- | 1583 | applys.ma | blob | raw |
-rw-r--r-- | 1593 | assumption.ma | blob | raw |
-rw-r--r-- | 1320 | bad_induction.ma | blob | raw |
drwxr-xr-x | - | bad_tests | tree |
-rw-r--r-- | 22961 | bool.ma | blob | raw |
-rw-r--r-- | 1747 | change.ma | blob | raw |
-rw-r--r-- | 1357 | clear.ma | blob | raw |
-rw-r--r-- | 1416 | clearbody.ma | blob | raw |
-rw-r--r-- | 4340 | coercions.ma | blob | raw |
-rw-r--r-- | 1708 | coercions_contravariant.ma | blob | raw |
-rw-r--r-- | 1501 | coercions_dependent.ma | blob | raw |
-rw-r--r-- | 1379 | coercions_dupelim.ma | blob | raw |
-rw-r--r-- | 1862 | coercions_nonuniform.ma | blob | raw |
-rw-r--r-- | 1588 | coercions_open.ma | blob | raw |
-rw-r--r-- | 4097 | coercions_propagation.ma | blob | raw |
-rw-r--r-- | 6134 | coercions_russell.ma | blob | raw |
-rw-r--r-- | 1443 | comments.ma | blob | raw |
-rw-r--r-- | 1769 | compose.ma | blob | raw |
-rw-r--r-- | 1227 | constructor.ma | blob | raw |
-rw-r--r-- | 2306 | continuationals.ma | blob | raw |
-rw-r--r-- | 1406 | contradiction.ma | blob | raw |
-rw-r--r-- | 1250 | cut.ma | blob | raw |
-rw-r--r-- | 6857 | decl.ma | blob | raw |
-rw-r--r-- | 1388 | decompose.ma | blob | raw |
-rw-r--r-- | 2004 | demodulation_coq.ma | blob | raw |
-rw-r--r-- | 1417 | demodulation_matita.ma | blob | raw |
-rw-r--r-- | 2133 | dependent_injection.ma | blob | raw |
-rw-r--r-- | 1150 | dependent_type_inference.ma | blob | raw |
-rw-r--r-- | 3048 | destruct.ma | blob | raw |
-rw-r--r-- | 2950 | elim.ma | blob | raw |
-rw-r--r-- | 4280 | fguidi.ma | blob | raw |
-rw-r--r-- | 1498 | first.ma | blob | raw |
-rw-r--r-- | 1434 | fix_betareduction.ma | blob | raw |
-rw-r--r-- | 1448 | fold.ma | blob | raw |
-rw-r--r-- | 1839 | generalize.ma | blob | raw |
-rw-r--r-- | 27520 | hard_refine.ma | blob | raw |
-rw-r--r-- | 2138 | injection.ma | blob | raw |
drwxr-xr-x | - | interactive | tree |
-rw-r--r-- | 2147 | inversion.ma | blob | raw |
-rw-r--r-- | 1975 | inversion2.ma | blob | raw |
-rw-r--r-- | 1340 | letrec.ma | blob | raw |
-rw-r--r-- | 1871 | letrecand.ma | blob | raw |
-rw-r--r-- | 985 | makefile | blob | raw |
-rw-r--r-- | 1910 | match_inference.ma | blob | raw |
-rw-r--r-- | 4236 | metasenv_ordering.ma | blob | raw |
-rw-r--r-- | 1973 | multiple_inheritance.ma | blob | raw |
-rw-r--r-- | 1104 | mysql_escaping.ma | blob | raw |
-rw-r--r-- | 1795 | naiveparamod.ma | blob | raw |
-rw-r--r-- | 1378 | overred.ma | blob | raw |
-rw-r--r-- | 1583 | paramodulation.ma | blob | raw |
drwxr-xr-x | - | paramodulation | tree |
-rw-r--r-- | 2123 | pullback.ma | blob | raw |
-rw-r--r-- | 1727 | record.ma | blob | raw |
-rw-r--r-- | 1914 | replace.ma | blob | raw |
-rw-r--r-- | 2641 | rewrite.ma | blob | raw |
-rw-r--r-- | 1362 | second.ma | blob | raw |
-rw-r--r-- | 1996 | simpl.ma | blob | raw |
-rw-r--r-- | 1990 | tacticals.ma | blob | raw |
-rw-r--r-- | 1339 | test2.ma | blob | raw |
-rw-r--r-- | 1436 | test3.ma | blob | raw |
-rw-r--r-- | 1480 | test4.ma | blob | raw |
-rw-r--r-- | 1368 | third.ma | blob | raw |
-rw-r--r-- | 1633 | tinycals.ma | blob | raw |
-rw-r--r-- | 1755 | unfold.ma | blob | raw |