Paul Brauner
@polux2001.bsky.social
I was using some library by Arthur Charguéraud I think, which was generating some boilerplate lemmas, if I remember correctly.
December 2, 2024 at 4:32 AM
I was using some library by Arthur Charguéraud I think, which was generating some boilerplate lemmas, if I remember correctly.
There was www.seas.upenn.edu/~plclub/popl... trying to settle that question for a while. I remember finding locally nameless nicer to work with than DB indices in coq.
The POPLmark Challenge
www.seas.upenn.edu
December 1, 2024 at 1:34 PM
There was www.seas.upenn.edu/~plclub/popl... trying to settle that question for a while. I remember finding locally nameless nicer to work with than DB indices in coq.