From 62085d29abb4e0eb2333541df4ed2735ad47f1cf Mon Sep 17 00:00:00 2001
From: hondet <gabrielhondet@gmail.com>
Date: Tue, 29 Jun 2021 19:34:40 +0200
Subject: [PATCH] transitivity with tuples

---
 personoj/examples/transitivity.lp | 13 ++++++++++---
 1 file changed, 10 insertions(+), 3 deletions(-)

diff --git a/personoj/examples/transitivity.lp b/personoj/examples/transitivity.lp
index bf4235e..b190fe5 100644
--- a/personoj/examples/transitivity.lp
+++ b/personoj/examples/transitivity.lp
@@ -11,7 +11,9 @@
 //                   real*
 //
 // And we coerce an element (in [foox]) from [real*] to [numfield*].
-require open personoj.lhol personoj.pvs_cert personoj.logical personoj.eqtup;
+require open
+  personoj.lhol personoj.pvs_cert personoj.logical personoj.eqtup
+  personoj.tuple;
 require open personoj.coercions;
 
 require open personoj.extra.equality;
@@ -26,8 +28,13 @@ symbol real ≔ psub {numfield} real_pred;
 symbol nz_real : El real → Prop;
 symbol real* ≔ psub {real} nz_real;
 
+// Symbols made to trigger coercions
+
 symbol foo : El numfield* → Prop;
+symbol foox : Π x: El real*, Prf (foo x)
+begin admit; end;
 
-debug +i;
-symbol foox : Π x: El real*, Prf (foo x) 
+// With a tuple
+symbol bar: El (σ numfield numfield*) → Prop;
+symbol barx : Π x: El real, Π y: El real*, Prf (bar (cons x y))
 begin admit; end;
-- 
GitLab