From 5f5dd7bc4cc167ca1603bb9650cf354bfb268e92 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?=E6=9D=BE=E4=B8=8B=E7=A5=90=E4=BB=8B?= <y.skm24t@gmail.com>
Date: Fri, 1 Apr 2022 19:07:46 +0900
Subject: [PATCH] Add a comment on type_soundness
---
theories/typing/soundness.v | 2 ++
1 file changed, 2 insertions(+)
diff --git a/theories/typing/soundness.v b/theories/typing/soundness.v
index ff8d2bb4..9fe2981c 100644
--- a/theories/typing/soundness.v
+++ b/theories/typing/soundness.v
@@ -28,6 +28,8 @@ Section type_soundness.
Definition main_transformer : predl_trans'ₛ [] () := (λ post '-[], post ()).
+ (* Intuitively, it says that execution of a closed, semantically well-typed
+ program, without any special precondition, does not get stuck *)
Theorem type_soundness `{!typePreG Σ} (main : val) σ t :
(∀ `{!typeG Σ}, typed_val main main_type main_transformer) →
rtc erased_step ([main [exit_cont]%E], ∅) (t, σ) →
--
GitLab