Skip to main content

Questions tagged [proof-review]

For questions that ask about possible improvements of a working piece of a proof. Make sure to also include the tag for the language used, and follow that tag's guidance regarding additional version-specific tags.

Filter by
Sorted by
Tagged with
5 votes
1 answer

How to implement first-order relational structures in Coq?

I'm trying to define a first-order relational structure in Coq. I have a way to define a pre-first-order-relational-structure, which is not a standard notion, but seems simple enough. I also have a ...
Greg Nisbet's user avatar
  • 2,829