summaryrefslogtreecommitdiff
path: root/LiftGet.agda
AgeCommit message (Expand)Author
2012-10-05move all postulates to one moduleHelmut Grohne
2012-09-27remove getVec-getlen in favour of plain substHelmut Grohne
2012-09-27move definition of get-type to BFF and use it everywhereHelmut Grohne
2012-09-14\::-subst is a special case of subst-congHelmut Grohne
2012-09-14vec-len-via-list and length-toList are the sameHelmut Grohne
2012-09-14complete missing parts of LiftGetHelmut Grohne
2012-09-11show fromList-toList in the subst formHelmut Grohne
2012-09-11LiftGet: replace vec-length-same with toList-substHelmut Grohne
2012-09-10LiftGet: vec-length is also known as subst (Vec A)Helmut Grohne
2012-09-04formulate List <-> Vec isomorphism problemsHelmut Grohne
2012-08-30prove LiftGet.get-trafo-2-getlenHelmut Grohne
2012-08-30phrase other half of bijection in LiftGetHelmut Grohne
2012-08-30prove half of the bijection in LiftGetHelmut Grohne
2012-08-30give the type of different gets a nameHelmut Grohne
2012-08-06attempt isomorphism between get on List and on VecHelmut Grohne
generated by cgit v1.2.3 (git 2.39.1) at 2025-07-01 23:21:08 +0000