Derive the constant map

diff --git a/vouivre/rules.scm b/vouivre/rules.scm
index 28f36d30ad91120fb448676006fc211563113aa4..5a784f3bc20ec421382f85bc4de50c6f32efdb49 100644 (file)
--- 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))