From 567280cb413c689ab4fc81c112f0aa9fca1fee3e Mon Sep 17 00:00:00 2001 From: Cameron Zwarich Date: Wed, 25 Jun 2025 15:16:36 -0700 Subject: [PATCH] chore: remove outdated comment (#9002) --- src/Lean/Compiler/LCNF/Basic.lean | 1 - 1 file changed, 1 deletion(-) diff --git a/src/Lean/Compiler/LCNF/Basic.lean b/src/Lean/Compiler/LCNF/Basic.lean index ee4235b23a..5bb80a6797 100644 --- a/src/Lean/Compiler/LCNF/Basic.lean +++ b/src/Lean/Compiler/LCNF/Basic.lean @@ -89,7 +89,6 @@ inductive LetValue where | proj (typeName : Name) (idx : Nat) (struct : FVarId) | const (declName : Name) (us : List Level) (args : Array Arg) | fvar (fvarId : FVarId) (args : Array Arg) - -- TODO: add constructors for mono and impure phases deriving Inhabited, BEq, Hashable def Arg.toLetValue (arg : Arg) : LetValue :=