index
:
~helmut/bidiragda.git
master
Bidirectionalization for Free in Agda (http://subdivi.de/~helmut/academia/fsbxia.pdf)
Helmut Grohne
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
BFF.agda
Age
Commit message (
Expand
)
Author
2019-09-29
port to agda/2.6.0.1 and agda-stdlib/1.1
Helmut Grohne
2018-11-25
port to agda/2.5.4.1 and agda-stdlib/0.17
Helmut Grohne
2015-06-09
drop barred members from GetTypes
Helmut Grohne
2014-04-03
drop PartialShapeVec
Helmut Grohne
2014-03-10
also allow Shaped types for the view
Helmut Grohne
2014-03-10
implement a bff on a shaped source type
Helmut Grohne
2014-03-07
use allFin rather than tabulate id
Helmut Grohne
2014-02-26
remove the sequenceV call from bff
Helmut Grohne
2014-02-17
Merge branch feature-partial-getlen into master
Helmut Grohne
2014-02-07
allow shape shape updates in bff
Helmut Grohne
2014-02-05
be more precise about which lookups we use
Helmut Grohne
2014-02-04
remove unused imports
Helmut Grohne
2014-02-04
add convenience members to PartialVecVec.Get
Helmut Grohne
2014-02-04
Merge branch feature-get-record into feature-partial-getlen
Helmut Grohne
2014-01-30
make the getlen functions explicit in PartialVecBFF
Helmut Grohne
2014-01-30
express VecBFF via PartialVecBFF
Helmut Grohne
2014-01-30
allow importing of Bidir without any postulates
Helmut Grohne
2014-01-30
pass get functions as records
Helmut Grohne
2014-01-28
define bff on a partial getlen
Helmut Grohne
2014-01-27
Merge branch feature-delete
Helmut Grohne
2014-01-23
generalize BFF and theorem-2 to arbitrary Setoids
Helmut Grohne
2014-01-17
generalize checkInsert to arbitrary Setoids
Helmut Grohne
2013-12-17
refactor to get rid of FinMap without Maybe entirely
Helmut Grohne
2013-12-17
update bff implementation to use delete
Helmut Grohne
2013-12-16
get rid of the ListBFF implementation
Helmut Grohne
2013-07-21
import _>>=_ and fmap from Data.Maybe
Helmut Grohne
2012-10-22
finally parameterize CheckInsert
Helmut Grohne
2012-10-22
now parameterize BFF
Helmut Grohne
2012-10-05
move all postulates to one module
Helmut Grohne
2012-10-05
remove VecRevBFF
Helmut Grohne
2012-09-27
move definition of get-type to BFF and use it everywhere
Helmut Grohne
2012-06-19
third definition of bff
Helmut Grohne
2012-06-05
make the Vec bff more similar to the List version
Helmut Grohne
2012-06-05
define a bff over Vec
Helmut Grohne
2012-06-05
move bff and friends to submodule ListBFF
Helmut Grohne