max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: remove outdated comment (#9002)

Browse source
This commit is contained in:
Cameron Zwarich 2025-06-25 15:16:36 -07:00 • committed by GitHub
parent 8da2f7105c
commit 567280cb41
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 0 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
src/Lean/Compiler/LCNF/Basic.lean
View file

@ -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 :=