Bas Spitters

Not sure whether this is related, but it gives some background on the idris editor and related work: https://cattheory.com/extensibleTypeDirectedEditing.pdf On Thu, Sep 6, 2018 at 5:37 PM Clément Pit-Claudel wrote:...

How about this? https://stackoverflow.com/questions/41837820/agda-like-programming-in-coq-proof-general or even the new Equations plug in ? On Thu, Sep 6, 2018 at 9:30 PM Clément Pit-Claudel wrote: > Right, that's what I meant by...

I seem to recall that lean just considers this a spelling error (using flyspeck). https://github.com/leanprover/lean-mode On Thu, Sep 6, 2018 at 10:07 PM Clément Pit-Claudel < [email protected]> wrote: > Hmm,...

After M-. on "list", I get taken to Init/Datatypes.v M-, gives "marker stack empty" Here are the TAGS keybindings: https://www.emacswiki.org/emacs/EmacsTags#toc1 On Mon, May 21, 2018 at 9:06 PM, Clément Pit-Claudel...

I'm on Ubuntu 18.04: emacs --version GNU Emacs 25.2.2 On Mon, May 21, 2018 at 9:21 PM, Clément Pit-Claudel < [email protected]> wrote: > Thanks. Is updating to a newer Emacs...

> What does M-: (fboundp 'xref-push-marker-stack) return? t > What about M-: (require 'xref)? xref > does M-. followed by M-, work after this require? Still the same error On...

I guess you've seen the primitive integers https://coq.github.io/doc/v8.11/refman/language/gallina-extensions.html#primitive-integers

Ignored instance declaration for “in_mon_unit_zero”: “ ∀ (K V : Type) (Ke : Equiv K) (Kplus : Plus K) (Kmult : Mult K) (Kzero : Zero K) (Kone : One...

@maximedenes What is the status of this?

About elliptic curves. We are currently considering whether it is feasible to integrate elliptic https://github.com/strub/elliptic-curves-ssr and fiat-crypto. So far things look positive. Is there a plan on integrating elliptic curves...