All Questions
Tagged with software-request coq
4
questions
2
votes
1
answer
70
views
Checking if a goal is *definitely wrong* by testing it against random examples in Coq
I'm currently poking around in a medium-sized Coq codebase that I didn't write and am not very familiar with ... and I'm trying off and on to make progress on some lemmas where the proof attempt was <...
- 3,095
2
votes
0
answers
65
views
Have Hyperdoctrines been formalized?
I was thinking of formalizing them myself for a project if they haven't been already, and I looked in libraries and couldn't find anything.
I was thinking of coq in particular because it's the only ...
- 143
5
votes
1
answer
186
views
List of general purpose Coq sublanguages for defining custom tactics
I've been tweaking the Coq plugin template recently to try to get a feel for writing custom Coq tactics in OCaml.
It's tricky. You need to define an .mlg file (...
- 3,095
10
votes
1
answer
268
views
Is there a Mizar-like sublanguage for Coq?
Isabelle has the frontend Isar which mimics some features of the Mizar system.
I'm curious if Coq has anything similar, i.e. an alternative to tactic scripts that's designed to be readable or similar ...
- 3,095