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

chore: share more code in toIRType (#9115)

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

17
src/Lean/Compiler/IR/ToIRType.lean
View file

@ -56,22 +56,21 @@ def toIRType (e : Lean.Expr) : CoreM IRType := do
| ``Float => return .float
| ``Float32 => return .float32
| ``lcErased => return .irrelevant
| _ =>
if let some scalarType ← lowerEnumToScalarType? name then
return scalarType
else
return .object
| _ => nameToIRType name
| .app f _ =>
-- All mono types are in headBeta form.
if let .const name _ := f then
if let some scalarType ← lowerEnumToScalarType? name then
return scalarType
else
return .object
nameToIRType name
else
return .object
| .forallE .. => return .object
| _ => panic! "invalid type"
where
nameToIRType name := do
if let some scalarType ← lowerEnumToScalarType? name then
return scalarType
else
return .object
inductive CtorFieldInfo where
| irrelevant