search

DmxLarchey / Breadth-First-Numbering

Coq implementation of Breadth-First Numbering à la Okasaki
Other
0 stars 0 forks source link

After submission (not urgent) #15

Open DmxLarchey opened 5 years ago

DmxLarchey commented 5 years ago

Dear Ralph,

When the submission is complete and you have some time, could you have a look at branch extend_llist file lazy_list.v which implements an isomorphism between lazy lists and list.

I find it is a nice development in Type theory with proofs of proof irrelevance ...

rmatthes commented 5 years ago

So, do you mean this would also be relevant from the point of view of univalent foundations?