Closed morganthomas closed 2 years ago
We can quantify over functions, lists, and maps. It would also be useful to be able to quantify over bijections, so that we can more efficiently arithmetize such quantification using a permutation argument.
This could take the form of adding a bijection type to the language.
Done.
We can quantify over functions, lists, and maps. It would also be useful to be able to quantify over bijections, so that we can more efficiently arithmetize such quantification using a permutation argument.