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

chore: remove redundant headBeta call (#8824)

Browse source
This commit is contained in:
Cameron Zwarich 2025-06-16 16:13:07 -07:00 • committed by GitHub
parent 46c3eaece9
commit 9e913a29de
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 2 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/Lean/Compiler/IR/ToIR.lean
View file

@ -110,7 +110,8 @@ def lowerType (e : Lean.Expr) : M IRType := do
else
return .object
| .app f _ =>
if let .const name _ := f.headBeta then
-- All mono types are in headBeta form.
if let .const name _ := f then
if let some scalarType ← lowerEnumToScalarType name then
return scalarType
else