From 5471d8bda928c703daad51263b79c11969c88a86 Mon Sep 17 00:00:00 2001
From: SimonGuilloud <simon.guilloud@epfl.ch>
Date: Wed, 10 Jan 2024 00:44:26 +0100
Subject: [PATCH] Lattices2 (#206)
Fix README to take the folder change of the reference manual into account. Small improvements to lattices tutorial.
---
README.md | 2 +-
lisa-examples/src/main/scala/Lattices.scala | 19 ++++++++++++++++++-
2 files changed, 19 insertions(+), 2 deletions(-)
diff --git a/README.md b/README.md
index 033651c4..237cd68b 100644
--- a/README.md
+++ b/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).
diff --git a/lisa-examples/src/main/scala/Lattices.scala b/lisa-examples/src/main/scala/Lattices.scala
index a2b49cb9..c4e7fba5 100644
--- a/lisa-examples/src/main/scala/Lattices.scala
+++ b/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
--
GitLab