Troubles loading the Logic Lab with shen-scheme

[Paolo Broglio]

Hello,

I'm currently reading "Logic, Proof and Computation" and have reached Lecture 6, which requires the use of the General Proof Assistant (GPA).

I've successfully loaded the GPA within Shen-scheme after loading StLib. However, when I attempt to use it, I encounter the following error:

(10-) (tc +)

true

(11+) (gpa)

1. p

type error: type p is not of type prop

I've documented the steps I've taken in this issue in the shen-scheme repository. 

I'm hoping to find a solution here, as I'm unsure how to resolve this error or if I'm overlooking something.

Thank you for your time.

PB

[Bruno Deferrari]

Repeating here what I think seems to be the issue.

The README mentions a System/FOL/loadme.shen file that I assume needs to be loaded to get the type theory, but it was not in the zip file.

The propositional calculus system discussed in the videos on the Shen Education channel
can be loaded from the directory Systems/FOL.  cd to this directory and type (load "loadme.shen").

I only see these in Systems/FOL:

external.shen

propositional.shen

quantificational.shen

syntax.shen

--
You received this message because you are subscribed to the Google Groups "Shen" group.
To unsubscribe from this group and stop receiving emails from it, send an email to qilang+un...@googlegroups.com.
To view this discussion, visit https://groups.google.com/d/msgid/qilang/d5ab2e94-f962-4c12-bee2-422cb184a996n%40googlegroups.com.

--

BD

[dr.mt...@gmail.com]

The programs for LPC live in their own space.  Unfotunately during recent spring cleaning

they got moved and I need to recalibrate the web site.  Meanwhile you can get them from

here.  Note you need a kernel with stlib installed.

Mark

[Paolo Broglio]

Oh i see. I've tried with the link you provided and now everything works! 

Thank you very much!

PB

[dr.mt...@gmail.com]

No problems; the download and support pages for LPC have been updated.

Mark