]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 876b7e9) | patch
we define the lazy poinwise extension of a relation, that should
authorFerruccio Guidi <ferruccio.guidi@unibo.it>
Sat, 8 Mar 2014 17:32:55 +0000 (17:32 +0000)
committerFerruccio Guidi <ferruccio.guidi@unibo.it>
Sat, 8 Mar 2014 17:32:55 +0000 (17:32 +0000)
commitebf2a09fa1fb0ae355ae97437f6e35377c5f2ae8
tree478b94b24cfe108050880b354c3e206d450530c6tree | snapshot
parent876b7e94113e67c7fb2dbc9ff7956c399778ce6fcommit | diff
we define the lazy poinwise extension of a relation, that should
allow to derive lleq with corrected lleq_lref, and a new defininition
for lpx (and derivatives), which now contains a bug too :( being not lazy
- we revise the definition of lazy equivakence since lleq_lref contains a bug
matita/matita/contribs/lambdadelta/basic_2/relocation/lleq.ma [new file with mode: 0644] blob
matita/matita/contribs/lambdadelta/basic_2/relocation/lleq_leq.ma [new file with mode: 0644] blob
matita/matita/contribs/lambdadelta/basic_2/relocation/llpx_sn.ma [new file with mode: 0644] blob
matita/matita/contribs/lambdadelta/basic_2/relocation/llpx_sn_leq.ma [new file with mode: 0644] blob
matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.