From afa06c6ac104217487b221abb27e81d2adda192e Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Franc=CC=A7ois=20Pottier?= <francois.pottier@inria.fr>
Date: Mon, 11 Nov 2024 13:54:22 +0100
Subject: [PATCH] Comments.

---
 coq/DemoSyntaxReduction.v | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/coq/DemoSyntaxReduction.v b/coq/DemoSyntaxReduction.v
index 4721df4..7436a73 100644
--- a/coq/DemoSyntaxReduction.v
+++ b/coq/DemoSyntaxReduction.v
@@ -31,6 +31,8 @@ Instance SubstLemmas_term : SubstLemmas term. derive. Qed.
 
 (* A demo of the tactics [autosubst] and [asimpl]. *)
 
+(* (λx. x y)[σ] = (λx. x y[⇑σ]) *)
+
 Goal
   forall sigma,
   (Lam (App (Var 0) (Var 1))).[sigma] =
@@ -106,6 +108,7 @@ Inductive red : term -> term -> Prop :=
     forall t1 t2 u,
     t1.[t2/] = u ->
     red (App (Lam t1) t2) u
+    (* (λx.t1) t2 → [t2/x]t1 *)
 
 (* Reduction in the left-hand side of an application. *)
 | RedAppL:
@@ -144,9 +147,11 @@ Local Hint Extern 1 (_ = _) => autosubst : autosubst.
 
 Definition Delta :=
   Lam (App (Var 0) (Var 0)).
+  (* Δ := λx.(x x) *)
 
 Definition Omega :=
   App Delta Delta.
+  (* Ω := (Δ Δ) *)
 
 Goal
   red Omega Omega.
-- 
GitLab