From 431698ade4b5c55b5128ec2a3ac61c886b2b624a Mon Sep 17 00:00:00 2001
From: hondet <gabrielhondet@gmail.com>
Date: Mon, 11 Oct 2021 15:31:44 +0200
Subject: [PATCH] Replace impd with unicode infix implication

---
 encoding/examples/rat.lp | 2 +-
 encoding/extra/if.lp     | 2 +-
 encoding/lhol.lp         | 4 ++--
 encoding/logical.lp      | 7 +++----
 4 files changed, 7 insertions(+), 8 deletions(-)

diff --git a/encoding/examples/rat.lp b/encoding/examples/rat.lp
index 885c5b5..598b58b 100644
--- a/encoding/examples/rat.lp
+++ b/encoding/examples/rat.lp
@@ -2,7 +2,7 @@ require open personoj.lhol;
 require open personoj.pvs_cert;
 
 // Prelude with some logics operator
-symbol ⇒ P Q ≔ impd {P} (λ _, Q);
+symbol ⇒ P Q ≔ P ⇒ (λ _, Q); // Use a non dependent implication
 notation ⇒ infix right 6;
 symbol false ≔ ∀ {prop} (λ x, x);
 symbol true ≔ false ⇒ false;
diff --git a/encoding/extra/if.lp b/encoding/extra/if.lp
index 2c77092..34db71d 100644
--- a/encoding/extra/if.lp
+++ b/encoding/extra/if.lp
@@ -4,7 +4,7 @@ require open personoj.lhol
              personoj.pvs_cert;
 
 symbol false ≔ ∀ {prop} (λ x, x);
-symbol true ≔ impd {false} (λ _, false);
+symbol true ≔ false ⇒ (λ _, false);
 
 symbol eq {s: Set}: El s → El s → El prop;
 symbol = {s} ≔ @eq s;
diff --git a/encoding/lhol.lp b/encoding/lhol.lp
index c9af629..d834dce 100644
--- a/encoding/lhol.lp
+++ b/encoding/lhol.lp
@@ -11,8 +11,8 @@ rule El prop ↪ Prop;
 constant symbol ∀ {x: Set}: (El x → Prop) → Prop;
 rule Prf (∀ {$X} $P) ↪ Π x: El $X, Prf ($P x);
 
-constant symbol impd {x: Prop}: (Prf x → Prop) → Prop;
-rule Prf (impd {$H} $P) ↪ Π h: Prf $H, Prf ($P h);
+constant symbol ⇒ (p: Prop): (Prf p → Prop) → Prop; notation ⇒ infix right 2;
+rule Prf ($P ⇒ $Q) ↪ Π h: Prf $P, Prf ($Q h);
 
 constant symbol arrd (x: Set): (El x → Set) → Set;
 rule El (arrd $X $T) ↪ Π x: El $X, El ($T x);
diff --git a/encoding/logical.lp b/encoding/logical.lp
index c7ebe31..a711962 100644
--- a/encoding/logical.lp
+++ b/encoding/logical.lp
@@ -1,10 +1,9 @@
 // Definition based on implication
 require open personoj.lhol;
 
-symbol ⇒ P Q ≔ impd {P} Q;             notation ⇒ infix right 2;
-symbol false ≔ ∀ {prop} (λ x, x);
-symbol true ≔ false ⇒ (λ _, false);
-symbol ¬ P ≔ impd {P} (λ _, false);    notation ¬ prefix 5;
+symbol false ≔ ∀ {prop} (λ x: El prop, x);
+symbol true ≔ false ⇒ (λ _: Prf false, false);
+symbol ¬ P ≔ P ⇒ (λ _, false);         notation ¬ prefix 5;
 symbol ∧ P Q ≔ ¬ (P ⇒ (λ h, ¬ (Q h))); notation ∧ infix 4;
 symbol ∨ P Q ≔ (¬ P) ⇒ Q;              notation ∨ infix 3;
 
-- 
GitLab