updated readme

README.org

@@ -56,7 +56,7 @@ If the RHS of a definition is =axiom=, then =perga= will assume that the identif
 
 Line comments are =--= like in Haskell, and block comments are =[* *]= somewhat like ML (and nest properly). There is no significant whitespace, so you are free to format code as you wish.
 
-There isn't a proper module system (yet), but you can include other files in a dumb, C preprocessor way by using =@include <filepath>= (NOTE: this unfortunately messes up line numbers in error messages). Filepaths are relative to the current file.
+There isn't a proper module system (yet), but you can include other files in a dumb, C preprocessor way by using =@include <filepath>= (NOTE: this unfortunately messes up line numbers in error messages). Filepaths are relative to the current file. Additionally, =@include= automatically keeps track of what has been included, so duplicate inclusions are skipped, meaning no include guards are necessary.
 
 * Usage
 Running =perga= without any arguments drops you into a basic repl. From here, you can type in definitions which =perga= will typecheck. Previous definitions are accessible in future definitions. The usual readline keybindings are available, including navigating history, which is saved between sessions (in =~/.cache/perga/history=). In the repl, you can enter ":q", press C-c, or press C-d to quit. Entering ":e" shows everything that has been defined along with their types. Entering ":t <ident>" prints the type of a particular identifier, while ":v <ident>" prints its value. Entering ":n <expr>" will fully normalize (including unfolding definitions) an expression, while ":w <expr>" will reduce it to weak head normal form. Finally ":l <filepath>" loads a file.
@@ -104,6 +104,7 @@ You can also give =perga= a filename as an argument, in which case it will typec
 * Simple Example
 There are many very well commented examples in the [[./examples/]] folder. These include
 - [[./examples/logic.pg]], which defines the standard logical operators and proves standard results about them,
+- [[./examples/classical.pg]], which asserts the law of the excluded middle as an axiom, and proves several results that require it,
 - [[./examples/computation.pg]], which demonstrates using =perga= for computational purposes,
 - [[./examples/algebra.pg]], which defines standard algebraic structures and proves results for them, and
 - [[./examples/peano.pg]], which proves standard arithmetic results from the Peano axioms.
@@ -133,12 +134,26 @@ Here is an example file defining Leibniz equality and proving that it is reflexi
 #+end_src
 Running =perga equality.pg= yields the following output.
 #+begin_src
-  eq : ∏ (A : *) . A -> A -> *
+  loading: equality.pg
-  eq_refl : ∏ (A : *) (x : A) . eq A x x
+  success!
-  eq_sym : ∏ (A : *) (x y : A) . eq A x y -> eq A y x
-  eq_trans : ∏ (A : *) (x y z : A) . eq A x y -> eq A y z -> eq A x z
 #+end_src
-This means our proofs were accepted. Furthermore, as a sanity check, we can see that the types correspond exactly to what we wanted to prove.
+This means our proofs were accepted.
+
+If we had an error in the proofs, we would get a somewhat useful error message. For example, if we had defined =eq_trans= as shown below, it would be incorrect (missing the =P= after =Hxy=).
+#+begin_src
+  eq_trans (A : *) (x y z : A) (Hxy : eq A x y) (Hyz : eq A y z) : eq A x z :=
+    fun (P : A -> *) (Hx : P x) => Hyz P (Hxy Hx);
+#+end_src
+Then running =perga equality.pg= yields the following output.
+#+begin_src 
+  loading: equality.pg
+  19:50:
+     |
+  19 |     fun (P : A -> *) (Hx : P x) => Hyz P (Hxy Hx);
+     |                                                  ^
+  Cannot unify 'A -> *' with 'P x' when evaluating 'Hxy Hx'
+#+end_src
+This indicates that, when evaluating =Hxy Hx=, it was expecting something of type =A -> *=, but instead found something of type =P x=. Since =P= is type =A -> *=, we can then realize that we forgot the =P=.
 
 * Future Goals