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

chore: use LitValue.toExpr instead of duplicating its definition (#8398)

Browse source
This commit is contained in:
Cameron Zwarich 2025-05-18 18:33:47 -07:00 • committed by GitHub
parent e7b8df0c0e
commit fbac0d2ddb
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 1 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -117,8 +117,7 @@ private unsafe def LetValue.updateArgsImp (e : LetValue) (args' : Array Arg) : L
def LetValue.toExpr (e : LetValue) : Expr :=
match e with
| .lit (.nat val) => .lit (.natVal val)
| .lit (.str val) => .lit (.strVal val)
| .lit v => v.toExpr
| .erased => erasedExpr
| .proj n i s => .proj n i (.fvar s)
| .const n us as => mkAppN (.const n us) (as.map Arg.toExpr)