Can't the language come with code that makes the
#lang acl2
line appear and disappear on write/read from the program's file?
As for sending it from drscheme to the ACL2 theorem prover, I
imagine that this is all under your control. -- Matthias
On Feb 1, 2010, at 2:16 PM, Carl Eastlund wrote:
On Mon, Feb 1, 2010 at 2:05 PM, Robby Findler
<[email protected]> wrote:
On Mon, Feb 1, 2010 at 1:03 PM, Carl Eastlund <[email protected]>
wrote:
On Mon, Feb 1, 2010 at 1:02 PM, Matthew Flatt <[email protected]>
wrote:
If a file extension is the only way to declare ACL2, then you'd
have to
save a file in DrScheme to use the ACL2 language.
I am fairly certain that other editors can save files with a ".lisp"
extension, so I don't know what you mean here.
He means that unsaved files won't know what language they are
supposed
to be in, I expect.
Oh, unsaved files. I see. What about just opening the Language menu
and selecting ACL2?
--Carl
_________________________________________________
For list-related administrative tasks:
http://list.cs.brown.edu/mailman/listinfo/plt-dev
_________________________________________________
For list-related administrative tasks:
http://list.cs.brown.edu/mailman/listinfo/plt-dev
