Stuck at first LPC proof

[Martin Clausen]

I recently bought the LPC book now got to Lecture 6 that requires Shen. I downloaded lpc.zip from http://www.shenlanguage.org/LPC/lpc.zip (btw the link at http://www.shenlanguage.org/lpc.htm is broken).

I got as far as step 1 of the the first proof but there I get the following:

(6+) (provedit!)


1. p
2. [p => q]
3. ^


>> q
=========================
Step 0 [1]


?- q


1. p
2. [p => q]


> =>1
Command not recognised; do you wish to abort the proof? (y/n)

I am on Windows 7 and have SBCL 1.3.6 installed.

[Mark Tarver]

Just gave it a bash

(2+) (provedit!)

1. p

2. [p => q]

3. ^

>> q

=========================

Step 0 [1]

?- q

1. p

2. [p => q]

> =>l

=========================

Step 1 [1]

?- p

1. p

2. [p => q]

> hyp

proved

save to file? (y/n)

Have you enabled the typechecker while loading?  provedit! type checks every command.

Next you need to put the provedit! program into the folder in which Shen is running.   To load this program, first type (tc +) and hit the return key then type (load "provedit!.shen").

 

(0-) (tc +)
true

 LPC p. 42

Mark

[Josh Tilles]

I believe you just entered a one when you should have entered an L—i.e., you entered =>1 instead of =>l.

I hope that helps!

[Martin Clausen]

That's it, thank you.