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

chore: remove special case for extern constructors (#10257)

Browse source 
This is subsumed by the fix in #10256.
This commit is contained in:
Cameron Zwarich 2025-09-04 23:08:45 -07:00 • committed by GitHub
parent de38a16fa9
commit 9923a8d9f8
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 0 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -160,9 +160,6 @@ partial def lowerLet (decl : LCNF.LetDecl) (k : LCNF.Code) : M FnBody := do
let env ← Lean.getEnv
match env.find? name with
| some (.ctorInfo ctorVal) =>
if isExtern env name then
return (← mkFap name irArgs)
let type ← nameToIRType ctorVal.induct
if type.isScalar then
let var ← bindVar decl.fvarId