source: README @ 18069

Using the typechecker.

Requirements:
1. OCaml and SPASS installed.
2. The PATH variable contains the SPASS executable .

Building:
cd src
make clean all

Running:
cd out
./typecheck ../../samples/simple.spi

Interpretting the results:
- "spass check results in true" means type-checking succeeded
- everything else means there was an error, e.g.
        - "Typechecking result: false" means that the type-checking  phase failed
        (you should use the "-v 1" or "-v 2" options for more details) 
        - "spass check results in false" means that the theorem proving phase failed
        (you can directly look at the file on which SPASS "exited with 1")


License:
   Copyright 2008 Stefan Lorenz, Kim Pecina, and Catalin Hritcu

   Licensed under the Apache License, Version 2.0 (the "License");
   you may not use this file except in compliance with the License.
   You may obtain a copy of the License at

       http://www.apache.org/licenses/LICENSE-2.0

   Unless required by applicable law or agreed to in writing, software
   distributed under the License is distributed on an "AS IS" BASIS,
   WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
   See the License for the specific language governing permissions and
   limitations under the License.