Skip to main content
2 events
when toggle format what by license comment
Aug 12, 2019 at 8:07 comment added darij grinberg I remember trying to figure out how to encode in Coq (in a programmatically verifiable way, not just as a comment) that two theorems are identical (this is the only way to provide two proofs for one theorem). Still no clue how to do that.
Aug 12, 2019 at 7:23 history answered Bjørn Kjos-Hanssen CC BY-SA 4.0