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)