]> matita.cs.unibo.it Git - helm.git/commit
- relations.ma:
authorFerruccio Guidi <ferruccio.guidi@unibo.it>
Wed, 28 Nov 2012 14:33:17 +0000 (14:33 +0000)
committerFerruccio Guidi <ferruccio.guidi@unibo.it>
Wed, 28 Nov 2012 14:33:17 +0000 (14:33 +0000)
commitb6a8600c3c4381809f1ab8d3e28628e17d9c3d3d
tree19682d4fe7697113ad82605d10b2c716c7326863
parent5876d7c2897e2d1f325fcddf8c243d47a5656e7c
- relations.ma:
  we introduced the reflexive closure (RC) for use in lambda and lambda_delta
- lambda:
  we introduced pointers to redexes
  notation bug fix in delifting_substitution.ma
matita/matita/contribs/lambda/delifting_substitution.ma
matita/matita/contribs/lambda/preamble.ma
matita/matita/contribs/lambda/redex_pointer.ma [new file with mode: 0644]
matita/matita/lib/basics/relations.ma