From: admin <admin@vouivredigital.com>
Date: Sat, 6 Apr 2024 17:58:14 +0000 (+0900)
Subject: Derive the constant map
X-Git-Url: https://git.vouivredigital.com/?a=commitdiff_plain;h=af3dc4749d5ea77479df05b0eecde9398f1d2425;p=vouivre.git

Derive the constant map
---

diff --git a/vouivre/rules.scm b/vouivre/rules.scm
index 28f36d3..5a784f3 100644
--- a/vouivre/rules.scm
+++ b/vouivre/rules.scm
@@ -290,3 +290,17 @@
   (ev #:index 0)
   (bool-elimination)
   (bool-formation))
+
+(define-derivation constant ((Γ (: y B) ⊢ (: (λ x y) (→ A B)))
+			     (Γ ⊢ (type A))
+			     (Γ ⊢ (type B)))
+  (λ)
+  (weakening #:index 1)
+  (exact)
+  (exact)
+  (weakening #:index 2)
+  (weakening #:index 1)
+  (exact)
+  (exact)
+  (generic-element #:index 1)
+  (exact))