coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Lean Theorem Prover

From: Arnaud Spiwack <aspiwack AT lix.polytechnique.fr>
To: Coq Club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Lean Theorem Prover
Date: Fri, 26 Feb 2016 07:23:59 +0100
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=arnaud.spiwack AT gmail.com; spf=Pass smtp.mailfrom=arnaud.spiwack AT gmail.com; spf=None smtp.helo=postmaster AT mail-lf0-f53.google.com
Ironport-phdr: 9a23:HppgtxU4FcIAk8BkuQnOzNnEr9PV8LGtZVwlr6E/grcLSJyIuqrYZhyHt8tkgFKBZ4jH8fUM07OQ6PC/HzJaqsfd+Fk5M7VyFDY9wf0MmAIhBMPXQWbaF9XNKxIAIcJZSVV+9Gu6O0UGUOz3ZlnVv2HgpWVKQka3CwN5K6zPF5LIiIzvjqbpq8KVPV8D1Wb1SIgxBSv1hD2ZjtMRj4pmJ/R54TryiVwMRd5rw3h1L0mYhRf265T41pdi9yNNp6BprJYYAu3SNp41Rr1ADTkgL3t9pIiy7UGCHkOz4S43VXxeuR5VCUCR5xbjG5z1ryHSt+xn2SDcM9egHp4uXjH3xr1tQQLkwBwfNiEw+2Kf3sVrlKNEqRmijxh+08jMZ4WEKPd1fqXcZM4XA2RbCJUCHxddC5+xOtNcR9EKOvxV+syk/wMD

I just mean I like the agda-style input which replaces \forall by the unicode ∀ seamlessly. It's possible that this is supported in coq as well I guess (I'm a little behind the times).

That's just built-in in emacs. There are even several ways to do that (the old-school quail, and the newish company-math at least).

Re: [Coq-Club] Lean Theorem Prover, (continued)
- Re: [Coq-Club] Lean Theorem Prover, Daniel Schepler, 02/25/2016
  - Re: [Coq-Club] Lean Theorem Prover, Abhishek Anand, 02/25/2016
    - Re: [Coq-Club] Lean Theorem Prover, Daniel Schepler, 02/26/2016
      - Re: [Coq-Club] Lean Theorem Prover, roux cody, 02/26/2016
        
        Re: [Coq-Club] Lean Theorem Prover, Jonathan Leivent, 02/26/2016
        
        Re: [Coq-Club] Lean Theorem Prover, Arnaud Spiwack, 02/26/2016
        
        Re: [Coq-Club] Lean Theorem Prover, Clément Pit--Claudel, 02/26/2016
        
        Re: [Coq-Club] Lean Theorem Prover, Benjamin C. Pierce, 02/26/2016
        RE: [Coq-Club] Lean Theorem Prover, Soegtrop, Michael, 02/26/2016
        Re: [Coq-Club] Lean Theorem Prover, Clément Pit--Claudel, 02/26/2016
        
        RE: [Coq-Club] Lean Theorem Prover, Makarius, 02/26/2016
        Re: [Coq-Club] Lean Theorem Prover, Clément Pit--Claudel, 02/26/2016
        
        Re: [Coq-Club] Lean Theorem Prover, Clément Pit--Claudel, 02/26/2016
        Re: [Coq-Club] Lean Theorem Prover, Makarius, 02/26/2016
        Re: [Coq-Club] Lean Theorem Prover, Clément Pit--Claudel, 02/27/2016
        Re: [Coq-Club] Lean Theorem Prover, Makarius, 02/27/2016