mattam82
commented
4 years ago I didn't try, but maybe others did. It could be that we lack some support somewhere, did you have an example of something you want to quote/unquote?
Open gmalecha opened 4 years ago
mattam82
commented
4 years ago I didn't try, but maybe others did. It could be that we lack some support somewhere, did you have an example of something you want to quote/unquote?
Are there any examples of people using the template monad to generate universe polymorphic code? I was having difficulty generating polymorphic lenses in the lens library: https://github.com/gmalecha/coq-lens/blob/master/theories/Lens.v