[opentheory-users] Fwd: Re: Is OpenTheory usable with Coq?

[Yannick]

------- Forwarded message -------
From: Yannick <yannick_duchene at yahoo.fr>
To: "Ramana Kumar" <ramana at member.fsf.org>
Cc:
Subject: Re: [opentheory-users] Is OpenTheory usable with Coq?
Date: Wed, 30 Dec 2015 02:46:31 +0100

On Tue, 29 Dec 2015 13:25:44 +0100, Ramana Kumar <ramana at member.fsf.org>  
wrote:

> I should add that for HOL4 (and HOL Light, I think) there are  
> editor-based interfaces (for Vim and for Emacs, at least) so >you are  
> not confined to using only the read-eval-print loop.

Precisely the two editors I'm afraid of :-D . Don't mind, I will setup  
what I need if I'm really not OK with the SML interpreter interface.


-- 
Yannick Duchêne



-- 
Yannick Duchêne
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.gilith.com/opentheory/mailing-list/attachments/20151230/c28ab136/attachment.html>