]> matita.cs.unibo.it Git - helm.git/tree - matita/matita/contribs/lambdadelta/basic_2/computation/
- the relation for pointwise extensions now takes a binder as argument
[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / computation /
drwxr-xr-x   ..
-rw-r--r-- 2625 acp.ma
-rw-r--r-- 5141 acp_aaa.ma
-rw-r--r-- 8824 acp_cr.ma
-rw-r--r-- 2517 cpds.ma
-rw-r--r-- 1432 cpds_aaa.ma
-rw-r--r-- 3953 cpds_cpds.ma
-rw-r--r-- 1857 cpds_lift.ma
-rw-r--r-- 1930 cpre.ma
-rw-r--r-- 1583 cpre_cpre.ma
-rw-r--r-- 6593 cprs.ma
-rw-r--r-- 7940 cprs_cprs.ma
-rw-r--r-- 2805 cprs_lift.ma
-rw-r--r-- 1938 cpxe.ma
-rw-r--r-- 8124 cpxs.ma
-rw-r--r-- 1674 cpxs_aaa.ma
-rw-r--r-- 9894 cpxs_cpxs.ma
-rw-r--r-- 1368 cpxs_leq.ma
-rw-r--r-- 6163 cpxs_lift.ma
-rw-r--r-- 2172 cpxs_lleq.ma
-rw-r--r-- 5347 cpxs_tstc.ma
-rw-r--r-- 9026 cpxs_tstc_vector.ma
-rw-r--r-- 5926 csx.ma
-rw-r--r-- 3131 csx_aaa.ma
-rw-r--r-- 4958 csx_alt.ma
-rw-r--r-- 1878 csx_fpbs.ma
-rw-r--r-- 5432 csx_lift.ma
-rw-r--r-- 1684 csx_lleq.ma
-rw-r--r-- 6710 csx_lpx.ma
-rw-r--r-- 1486 csx_lpxs.ma
-rw-r--r-- 5770 csx_tstc_vector.ma
-rw-r--r-- 2080 csx_vector.ma
-rw-r--r-- 1864 fpbc.ma
-rw-r--r-- 1967 fpbc_fleq.ma
-rw-r--r-- 1544 fpbc_fpbs.ma
-rw-r--r-- 3541 fpbg.ma
-rw-r--r-- 4080 fpbg_fleq.ma
-rw-r--r-- 2802 fpbg_fpbg.ma
-rw-r--r-- 1739 fpbg_lift.ma
-rw-r--r-- 8376 fpbs.ma
-rw-r--r-- 1618 fpbs_aaa.ma
-rw-r--r-- 4384 fpbs_alt.ma
-rw-r--r-- 2018 fpbs_ext.ma
-rw-r--r-- 1454 fpbs_fleq.ma
-rw-r--r-- 1300 fpbs_fpbs.ma
-rw-r--r-- 2156 fpbs_lift.ma
-rw-r--r-- 2510 fpbu.ma
-rw-r--r-- 3509 fpbu_fleq.ma
-rw-r--r-- 1872 fpbu_lift.ma
-rw-r--r-- 1972 fpbu_lleq.ma
-rw-r--r-- 2283 fsb.ma
-rw-r--r-- 3886 fsb_aaa.ma
-rw-r--r-- 4010 fsb_alt.ma
-rw-r--r-- 3532 fsb_csx.ma
-rw-r--r-- 3594 lcosx.ma
-rw-r--r-- 3562 lcosx_cpx.ma
-rw-r--r-- 3235 lprs.ma
-rw-r--r-- 7073 lprs_cprs.ma
-rw-r--r-- 1569 lprs_ldrop.ma
-rw-r--r-- 1595 lprs_lprs.ma
-rw-r--r-- 3618 lpxs.ma
-rw-r--r-- 1714 lpxs_aaa.ma
-rw-r--r-- 8658 lpxs_cpxs.ma
-rw-r--r-- 1593 lpxs_ldrop.ma
-rw-r--r-- 6605 lpxs_lleq.ma
-rw-r--r-- 1291 lpxs_lpxs.ma
-rw-r--r-- 5028 lsubc.ma
-rw-r--r-- 3675 lsubc_ldrop.ma
-rw-r--r-- 1870 lsubc_ldrops.ma
-rw-r--r-- 1535 lsubc_lsuba.ma
-rw-r--r-- 4536 lsx.ma
-rw-r--r-- 5397 lsx_alt.ma
-rw-r--r-- 3073 lsx_csx.ma
-rw-r--r-- 4626 lsx_ldrop.ma
-rw-r--r-- 3105 lsx_lpx.ma
-rw-r--r-- 3116 lsx_lpxs.ma