[plt-dev] #lang: the stake in Dracula's heart?

From: Matthias Felleisen (matthias at ccs.neu.edu)
Date: Mon Feb 1 14:26:52 EST 2010

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
> <robby at eecs.northwestern.edu> wrote:
>> On Mon, Feb 1, 2010 at 1:03 PM, Carl Eastlund <cce at ccs.neu.edu>  
>> wrote:
>>> On Mon, Feb 1, 2010 at 1:02 PM, Matthew Flatt <mflatt at cs.utah.edu>  
>>> 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

Posted on the dev mailing list.