LP is a command-driven system. The last line of LP's welcoming message, LP1:, is a prompt for the first command. LP prompts users to enter subsequent commands with LP2:, LP3:, ...Welcome to LP (the Larch Prover), Release 3.1 (94/12/30). Copyright (C) 1994, S. J. Garland and J. V. Guttag Type `help lp' (followed by a carriage return) for help. LP1:
You can type input directly in response to LP's prompts, or you can create a file of LP commands (e.g., set1.lp) and then use LP's execute command to cause LP to execute the commands in that file as if you had typed them directly. Here's the start of a session in which commands are executed from the file set1.lp:
The first command, execute set1, was typed by the user. The second was obtained from the file set1.lp. This command is a comment: LP ignores all input following a percent sign. The prompts LP1.1: and LP1.2: indicate that LP is taking input from the file being executed as a result of the command entered in response to the prompt LP1:.LP1: execute set1 LP1.1: % Some simple theorems about finite sets LP1.2: