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

chore: missing @[specialize]

Browse source
This commit is contained in:
Leonardo de Moura 2019-11-04 03:59:39 -08:00
parent 1bf1290570
commit cf17fbb8e9
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
library/Init/Lean/TypeUtil.lean
View file

@ -152,7 +152,7 @@ else
if args.size < 2 then e
else mkAppRange (args.get! 1) 2 args.size args
private def deltaBetaDefinition {α} (c : ConstantInfo) (lvls : List Level) (revArgs : Array Expr) (failK : Unit → α) (successK : Expr → α) : α :=
@[specialize] private def deltaBetaDefinition {α} (c : ConstantInfo) (lvls : List Level) (revArgs : Array Expr) (failK : Unit → α) (successK : Expr → α) : α :=
if c.lparams.length != lvls.length then failK ()
else
let val := c.instantiateValueLevelParams lvls;