From ea41b63e62fa6ba2327cc396e0fcfe922a4b987e Mon Sep 17 00:00:00 2001
From: hondet <gabrielhondet@gmail.com>
Date: Tue, 29 Jun 2021 18:30:33 +0200
Subject: [PATCH] added transitivity example
---
personoj/examples/transitivity.lp | 33 +++++++++++++++++++++++++++++++
1 file changed, 33 insertions(+)
create mode 100644 personoj/examples/transitivity.lp
diff --git a/personoj/examples/transitivity.lp b/personoj/examples/transitivity.lp
new file mode 100644
index 0000000..bf4235e
--- /dev/null
+++ b/personoj/examples/transitivity.lp
@@ -0,0 +1,33 @@
+// This file shows that coercions are transitive.
+// We have approximately the following setup
+//
+// numfield
+// / \
+// / \
+// / \
+// numfield* real
+// |
+// |
+// 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.coercions;
+
+require open personoj.extra.equality;
+
+constant symbol numfield: Set;
+constant symbol nz_numfield : El numfield → Prop;
+symbol numfield* ≔ psub {numfield} nz_numfield;
+
+constant symbol real_pred : El numfield → Prop;
+symbol real ≔ psub {numfield} real_pred;
+
+symbol nz_real : El real → Prop;
+symbol real* ≔ psub {real} nz_real;
+
+symbol foo : El numfield* → Prop;
+
+debug +i;
+symbol foox : Î x: El real*, Prf (foo x)
+begin admit; end;
--
GitLab