projects / ~helmut / bidiragda.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 50f61be) | patch
FinMap.lemma-lookupM-fromFunc is almost Data.Vec.Properties.lookup∘tabulate
authorHelmut Grohne <helmut@subdivi.de>
Sun, 31 Mar 2019 19:47:21 +0000 (21:47 +0200)
committerHelmut Grohne <helmut@subdivi.de>
Sun, 31 Mar 2019 19:47:21 +0000 (21:47 +0200)
commit121094635514bf07bb91d6b7d16a45674c74f34e
treec7f9c952c05774fd78d9c25e615b0a4da26d6846tree | snapshot
parent50f61bef184194fc48dd1415800830d032495f51commit | diff
FinMap.lemma-lookupM-fromFunc is almost Data.Vec.Properties.lookup∘tabulate
Bidir.agda diff | blob | history
FinMap.agda diff | blob | history
Precond.agda diff | blob | history
Bidirectionalization for Free in Agda (http://subdivi.de/~helmut/academia/fsbxia.pdf)