summaryrefslogtreecommitdiff
path: root/GetTypes.agda
AgeCommit message (Expand)Author
2015-06-09drop barred members from GetTypesHelmut Grohne
2015-06-09drop the Function.Equality requirement from GetTypesHelmut Grohne
2014-10-14drop the injection requirement for gl₁Helmut Grohne
2014-04-03drop PartialShapeVecHelmut Grohne
2014-03-10also allow Shaped types for the viewHelmut Grohne
2014-03-10implement a bff on a shaped source typeHelmut Grohne
2014-02-04add convenience members to PartialVecVec.GetHelmut Grohne
2014-02-04Merge branch feature-get-record into feature-partial-getlenHelmut Grohne
2014-01-30allow importing of Bidir without any postulatesHelmut Grohne