Skip to Content.
Sympa Menu

coq-club - [Coq-Club] Formatting ssreflect proofs

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Formatting ssreflect proofs


Chronological Thread 
  • From: kirang <kirang AT comp.nus.edu.sg>
  • To: coq-club AT inria.fr
  • Subject: [Coq-Club] Formatting ssreflect proofs
  • Date: Tue, 01 Oct 2019 12:22:52 +0800
  • Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=kirang AT comp.nus.edu.sg; spf=Pass smtp.mailfrom=kirang AT comp.nus.edu.sg; spf=None smtp.helo=postmaster AT mailgw0.comp.nus.edu.sg
  • Ironport-phdr: 9a23:5UBzphbOrHkAs+YlpiRt6/n/LSx+4OfEezUN459isYplN5qZocW8bnLW6fgltlLVR4KTs6sC17ON9fy7EjNQqb+681k6OKRWUBEEjchE1ycBO+WiTXPBEfjxciYhF95DXlI2t1uyMExSBdqsLwaK+i764jEdAAjwOhRoLerpBIHSk9631+ev8JHPfglEnjWwba58IRmsogjcuMYajIlhJ60s1hbHv3xEdvhMy2h1P1yThRH85smx/J5n7Stdvu8q+tBDX6vnYak2VKRUAzs6PW874s3rrgTDQhCU5nQASGUWkwFHDBbD4RrnQ5r+qCr6tu562CmHIc37SK0/VDq+46t3ThLjlSEKPCM7/m7KkMx9lK1Urw6uqRJxw4DafpybOvlxf6zTZt4aWWhMXsRNWyBdGI6wcY0CBPcBM+ZCqIn9okMDrRi/BQm2HuzvzDBIjWLx0K050uQhCxvJ3AovH98VrHvUq9D1NL8IXeCz0anI1i/PYO1L1jfg8oTIaR8hrOiKULltcsTR0VEiGx7Lg1iSs4DpIj2Y2voXv2WY4OdsT/yjh3IhpgpsuDag3N0shZPMho8NylDL6yF5wIEtKN29UkF7YNqkEJReti2GLYd5XsQiQ2RwuCogzL0GpIW7cDIUx5s62h7TceeHc4eQ7hLiUuaePyt4iWp4dL+xhRu+61Wsx+PiWsWu01tHoTBJnsfQunwV0hzc8MmHSv9z/ke73jaP0hje6uJFIUAuj6XbLZEhz6UsmZoUtETDBjX6mEPrjK+NbEkr5PWn6/n9brX9qZ+QL5V0hR3mMqQyhsy/Bvw1PRQJX2iC4OizyLnj/VDiT7hRlf03kqzZsIjAKsgBp665BRVV0oc55BqlATemyodQoX5SJ1VcPRmDkoLBOlfUIfm+A+3srU6rlWJoxurPOLKpVpbMNHHFn5/qerNlrUhB00w+wc0Z/J0CWeJJG+76RkKk7I+QNRQ+KQHhm7+6WuU47ZsXXCe0OoHcMK7WtgXVtOcmIu2De9dTszH4M74j+uWogHMk30QSL/HwjMknLUugF/EjGH23JH/lg9MPC2AP51VsR+vvkBuETCUVanqvGbkztGhiVNCWSLzbT4Xou4SvmT+hF8QJNGtBD0jKF2rzMYiIRrEXZ3DKLw==

Dear Coq Club,

I was wondering if there was any standard tools for formatting coq proofs (or any specifically for proofs using ssreflect)?

I've been using proof general in emacs with the built-in formatter, but a lot of times I end up fighting it, leading to odd indentation.


Thanks.
-----
Kiran Gopinathan,
PhD Candidate, NUS,
Singapore


  • [Coq-Club] Formatting ssreflect proofs, kirang, 10/01/2019

Archive powered by MHonArc 2.6.18.

Top of Page