turns out: ind-cong is a special case of H.congâ‚‚
[~helmut/bidiragda.git] / LiftGet.agda
2015-01-05 Helmut Grohneturns out: ind-cong is a special case of H.congâ‚‚
2014-02-26 Helmut Grohneconvert LiftGet module to using heterogeneous equality
2014-02-04 Helmut GrohneMerge branch feature-get-record into feature-partial...
2014-02-03 Helmut GrohneMerge branch feature-get-record into master
2014-02-03 Helmut Grohnealso show the other direction GetL-to-GetV
2014-02-03 Helmut Grohneadd a GetV-to-GetL transformer
2014-01-30 Helmut Grohnepass get functions as records
2013-12-16 Helmut Grohnemove generic functions to a new Generic module
2012-10-05 Helmut Grohnemove all postulates to one module
2012-09-27 Helmut Grohneremove getVec-getlen in favour of plain subst
2012-09-27 Helmut Grohnemove definition of get-type to BFF and use it everywhere
2012-09-18 Helmut GrohneMerge branch 'using-vec'
2012-09-14 Helmut Grohne\::-subst is a special case of subst-cong
2012-09-14 Helmut Grohnevec-len-via-list and length-toList are the same
2012-09-14 Helmut Grohnecomplete missing parts of LiftGet
2012-09-11 Helmut Grohneshow fromList-toList in the subst form
2012-09-11 Helmut GrohneLiftGet: replace vec-length-same with toList-subst
2012-09-10 Helmut GrohneLiftGet: vec-length is also known as subst (Vec A)
2012-09-04 Helmut Grohneformulate List <-> Vec isomorphism problems
2012-08-30 Helmut Grohneprove LiftGet.get-trafo-2-getlen
2012-08-30 Helmut Grohnephrase other half of bijection in LiftGet
2012-08-30 Helmut Grohneprove half of the bijection in LiftGet
2012-08-30 Helmut Grohnegive the type of different gets a name
2012-08-06 Helmut Grohneattempt isomorphism between get on List and on Vec