Closed yurrriq closed 7 years ago
One idea might be to leave some of the SF-in-Coq completely intact (like the Preface). Then introduce a Preface for SF-in-Idris if you like.
Not a bad idea...
Might want to mention Idris here: https://github.com/idris-hackers/software-foundations/blob/fc6fc1ecc4ab5b337f9afe59cd57c0142b454546/src/Preface.lidr#L109
Closing to simplify tracking on #20.
For now, it's copied rather directly from the Coq.