diff options
| author | Helmut Grohne <helmut@subdivi.de> | 2012-09-04 08:42:38 +0200 |
|---|---|---|
| committer | Helmut Grohne <helmut@subdivi.de> | 2012-09-04 08:42:38 +0200 |
| commit | bd2a63675bb859e42d9e1464ff9a7883884c1fd5 (patch) | |
| tree | 08d70e85b7016ae81376f945c3f905f809b05ff2 /Bidir.agda | |
| parent | 22d4d452aaee82744c57f063b3416fd67df736c2 (diff) | |
| download | bidiragda-bd2a63675bb859e42d9e1464ff9a7883884c1fd5.tar.gz | |
formulate List <-> Vec isomorphism problems
There are now like four open holes in LiftGet.agda that all boil down to
the same problem. For proving equalities on Vec we first need to show
that those Vecs actually have the same type. Proofs on two different
levels are needed and somehow need to be merged.
Diffstat (limited to 'Bidir.agda')
0 files changed, 0 insertions, 0 deletions