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

fix: bad message

Browse source
This commit is contained in:
Leonardo de Moura 2020-09-25 11:16:52 -07:00
parent eae32b08a6
commit 049ff2b022
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/Lean/Compiler/Specialize.lean
View file

@ -27,8 +27,8 @@ end SpecializeAttributeKind
def mkSpecializeAttrs : IO (EnumAttributes SpecializeAttributeKind) :=
registerEnumAttributes `specializeAttrs
[(`specialize, "mark definition to always be inlined", SpecializeAttributeKind.specialize),
(`nospecialize, "mark definition to never be inlined", SpecializeAttributeKind.nospecialize) ]
[(`specialize, "mark definition to always be specialized", SpecializeAttributeKind.specialize),
(`nospecialize, "mark definition to never be specialized", SpecializeAttributeKind.nospecialize) ]
/- TODO: fix the following hack.
We need to use the following hack because the equation compiler generates auxiliary
definitions that are compiled before we even finish the elaboration of the current command.