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

chore: update builtin_widget_module registration code

Browse source
This commit is contained in:
Sebastian Ullrich 2024-02-19 12:33:23 +01:00
parent da24708ba5
commit 032a2ecaa1
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/Lean/Widget/UserWidget.lean
View file

@ -102,7 +102,7 @@ builtin_initialize widgetModuleAttrImpl : AttributeImpl ←
let env ← getEnv
if builtin then
let h := mkConst decl
declareBuiltin decl <| mkApp (mkConst ``addBuiltinModule) h
declareBuiltin decl <| mkApp2 (mkConst ``addBuiltinModule) (toExpr decl) h
else
setEnv <| moduleRegistry.addEntry env (mod.javascriptHash, decl, e)
}