From 54e4cfa8e267bf604afba67357b16a45d97ad88f Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 24 Aug 2022 06:55:51 -0700
Subject: [PATCH] chore: doc string

---
 src/Lean/Compiler/LCNF/ToLCNF.lean | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/src/Lean/Compiler/LCNF/ToLCNF.lean b/src/Lean/Compiler/LCNF/ToLCNF.lean
index 110482a21b..340a7adadb 100644
--- a/src/Lean/Compiler/LCNF/ToLCNF.lean
+++ b/src/Lean/Compiler/LCNF/ToLCNF.lean
@@ -23,6 +23,11 @@ def isLCProof (e : Expr) : Bool :=
 def mkLcProof (p : Expr) :=
   mkApp (mkConst ``lcProof []) p
 
+/--
+Auxiliary inductive datatype for constructing LCNF `Code` objects.
+The `toLCNF` function maintains a sequence of elements that is eventually
+converted into `Code`.
+-/
 inductive Element where
   | jp  (decl : FunDecl)
   | fun (decl : FunDecl)