summaryrefslogtreecommitdiff
path: root/GetTypes.agda
AgeCommit message (Collapse)Author
2014-02-04add convenience members to PartialVecVec.GetHelmut Grohne
2014-02-04Merge branch feature-get-record into feature-partial-getlenHelmut Grohne
These two features heavily interconnect. As such it makes sense to integrate them properly. This non-trivial merge does that work. Compared to feature-partial-getlen a few definitions moved from FreeTheorems.agda to GetTypes.agda. Many types changed compared to both branches. Conflicts: BFF.agda Bidir.agda FreeTheorems.agda Precond.agda conflict in GetTypes.agda not detected by merge
2014-01-30allow importing of Bidir without any postulatesHelmut Grohne