Lattices2 (#206)

Fix README to take the folder change of the reference manual into account. Small improvements to lattices tutorial.

README.md

@@ -2,7 +2,7 @@
 
 LISA is a proof assistant based on first-order logic, sequent calculus, and set
 theory. To get started, take a look at the [Reference
-Manual](Reference%20Manual/lisa.pdf).
+Manual](refman/lisa.pdf).
 
 LISA is developed and maintained by the [Laboratory for Automated Reasoning and
 Analysis (LARA)](https://lara.epfl.ch) at the [EPFL](https://epfl.ch).

lisa-examples/src/main/scala/Lattices.scala

@@ -1,4 +1,22 @@
 object Lattices extends lisa.Main {
+
+
+
+  val x = variable
+  val P = predicate[1]
+  val f = function[1]
+
+  val fixedPointDoubleApplication = Theorem(
+    ∀(x, P(x) ==> P(f(x))) |- P(x) ==> P(f(f(x)))
+  ) {
+    sorry
+  }
+
+
+
+
+
+
   // We introduce the signature of lattices
   val <= = ConstantPredicateLabel.infix("<=", 2)
   addSymbol(<=)
@@ -16,7 +34,6 @@ object Lattices extends lisa.Main {
 
   // We now states the axioms of lattices
 
-  val x = variable
   val y = variable
   val z = variable