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