From 88d56a027c77b5360e37cd055a001f91b992f89c Mon Sep 17 00:00:00 2001
From: gabrielhdt <gabrielhondet@gmail.com>
Date: Fri, 22 May 2020 18:32:34 +0200
Subject: [PATCH] pred as a definition, nothing more

---
 prelude/logic.lp | 16 +++++++---------
 1 file changed, 7 insertions(+), 9 deletions(-)

diff --git a/prelude/logic.lp b/prelude/logic.lp
index 80c2ec4..e04d305 100644
--- a/prelude/logic.lp
+++ b/prelude/logic.lp
@@ -29,9 +29,8 @@ require open personoj.encodings.builtins
 // boolean_props
 // Slightly modified from the prelude
 constant symbol bool_exclusive: ε (neq {bool} false true)
-constant
-symbol bool_inclusive
-     : ε (∀ {bool} (λa, ((eq {bool} a false) ∨ (λ_, eq {bool} a true))))
+constant symbol bool_inclusive:
+  ε (∀ {bool} (λa, ((eq {bool} a false) ∨ (λ_, eq {bool} a true))))
 
 theorem excluded_middle: ε (∀ {bool} (λa, a ∨ (λ_, ¬ a)))
 proof
@@ -46,9 +45,9 @@ definition xor (a b: η bool) ≔ neq {bool} a b
 
 // PVS solves that kind of things thanks to the (bddsimp) tactic which uses an
 // external C program
-theorem xor_def
-      : ε (∀ {bool} (λa, ∀ {bool} (λb, eq {bool} (xor a b)
-                                          (if {bool} a (λ_, ¬ b) (λ_, b)))))
+theorem xor_def:
+  ε (∀ {bool} (λa, ∀ {bool} (λb, eq {bool} (xor a b)
+                                    (if {bool} a (λ_, ¬ b) (λ_, b)))))
 proof
   set prover "Alt-Ergo"
   set prover_timeout 12
@@ -61,9 +60,8 @@ admit
 //
 // Defined types
 //
-// FIXME: needs another prenex polymorphism to be encoded,
-require open personoj.encodings.pvs_more
-definition pred : ι ({|set|} *> {|set|}) ≔ λt: θ {|set|}, t ~> bool
+// NOTE ‘pred’ cannot be typed in the encoding
+definition pred (t: θ {|set|}) ≔ t ~> bool
 definition PRED ≔ pred
 definition predicate ≔ pred
 definition PREDICATE ≔ pred
-- 
GitLab