From 5ecd07e3a0de8fd0fedabdf80e65122ec72bfcbe Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Blanqui?= <frederic.blanqui@inria.fr>
Date: Tue, 19 Nov 2024 14:27:45 +0100
Subject: [PATCH 1/3] add files for HOL

---
 Epsilon.lp | 4 ++++
 HOL.lp     | 5 +++++
 Impred.lp  | 5 +++++
 Set.lp     | 2 ++
 4 files changed, 16 insertions(+)
 create mode 100644 Epsilon.lp
 create mode 100644 HOL.lp
 create mode 100644 Impred.lp

diff --git a/Epsilon.lp b/Epsilon.lp
new file mode 100644
index 0000000..07bfd2d
--- /dev/null
+++ b/Epsilon.lp
@@ -0,0 +1,4 @@
+require open Stdlib.Set Stdlib.Prop Stdlib.FOL;
+
+symbol ε [a:Set] : (τ a → Prop) → τ a;
+symbol εᵢ [a:Set] (p:τ a → Prop) : π (∃ p) → π (p (ε p));
diff --git a/HOL.lp b/HOL.lp
new file mode 100644
index 0000000..153eb26
--- /dev/null
+++ b/HOL.lp
@@ -0,0 +1,5 @@
+require open Stdlib.Set;
+
+symbol ⤳ : Set → Set → Set; notation ⤳ infix right 10;
+
+rule τ ($x ⤳ $y) ↪ τ $x → τ $y;
diff --git a/Impred.lp b/Impred.lp
new file mode 100644
index 0000000..38b5eb3
--- /dev/null
+++ b/Impred.lp
@@ -0,0 +1,5 @@
+require open Stdlib.Set Stdlib.Prop;
+
+symbol o : Set;
+
+rule τ o ↪ Prop;
diff --git a/Set.lp b/Set.lp
index 16d3539..086e526 100644
--- a/Set.lp
+++ b/Set.lp
@@ -2,6 +2,8 @@
 
 constant symbol Set : TYPE;
 
+constant symbol ι : Set;
+
 // Interpretation of set codes in TYPE
 
 injective symbol τ : Set → TYPE; // `t or \tau

From 66280ffb3a4481cb63b61e34b8c4faa7457f6393 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Blanqui?= <frederic.blanqui@inria.fr>
Date: Tue, 19 Nov 2024 14:33:29 +0100
Subject: [PATCH 2/3] update CHANGES

---
 CHANGES.md | 17 +++++++++++------
 1 file changed, 11 insertions(+), 6 deletions(-)

diff --git a/CHANGES.md b/CHANGES.md
index 0ddb7de..3e7bc1e 100644
--- a/CHANGES.md
+++ b/CHANGES.md
@@ -5,18 +5,23 @@ and this project adheres to [Semantic Versioning](https://semver.org/).
 
 ## Unreleased
 
-- Declare istrue as injective
+- Add files for higher-order logic:
+  HOL: Set constructor ⤳ for quantifying over function types
+  Impred: Set constructor o for quantifying over propositions
+  Epsilon: Hilbert's ε operator
+- Set: add ι:Set
+- Bool: declare istrue as injective
 
 ## 1.1.0 (2024-06-21)
 
-- Add classical logic
-- Rename top into ⊤ᵢ
-- Declare more arguments of ∃ᵢ and ∃ₑ implicit
+- Classic: classical logic
+- Prop: rename top into ⊤ᵢ
+- FOL: declare more arguments of ∃ᵢ and ∃ₑ implicit
 
 ## 1.0.0 (2023-10-19)
 
-- Add integers (Quentin Garchery)
+- Z: integers (Quentin Garchery)
 
 ## 0.0.0 (2022-01-27)
 
-- Add natural numbers and lists (Quentin Buzet)
+- Nat, List: natural numbers and lists (Quentin Buzet)

From cab9997705bca66474c89880d5903e98ba0ad29c Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Blanqui?= <frederic.blanqui@inria.fr>
Date: Tue, 19 Nov 2024 14:36:25 +0100
Subject: [PATCH 3/3] wip

---
 HOL.lp | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/HOL.lp b/HOL.lp
index 153eb26..8bb76f7 100644
--- a/HOL.lp
+++ b/HOL.lp
@@ -1,5 +1,7 @@
 require open Stdlib.Set;
 
-symbol ⤳ : Set → Set → Set; notation ⤳ infix right 10;
+symbol ⤳ : Set → Set → Set; // \leadsto
+
+notation ⤳ infix right 20;
 
 rule τ ($x ⤳ $y) ↪ τ $x → τ $y;