From e8628f60a6e436a26ba50f2c5e20501620a9e489 Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Thu, 18 May 2017 18:00:00 +0200
Subject: [PATCH] Comment on function type.

---
 theories/typing/function.v | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/theories/typing/function.v b/theories/typing/function.v
index 44a158ad..5bf28346 100644
--- a/theories/typing/function.v
+++ b/theories/typing/function.v
@@ -15,6 +15,11 @@ Section fn.
                     ty.(ty_wf_E) ++ ty.(ty_outlives_E) ϝ)
        tys ty.
 
+  (* The other alternative for defining the fn type would be to state
+     that the value applied to its parameters is a typed body whose type
+     is the return type.
+     That would be slightly simpler, but, unfortunately, we are no longer
+     able to prove that this is contractive. *)
   Program Definition fn (fp : A → fn_params) : type :=
     {| st_own tid vl := (∃ fb kb xb e H,
          ⌜vl = [@RecV fb (kb::xb) e H]⌝ ∗ ⌜length xb = n⌝ ∗
-- 
GitLab