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

chore: simplify signature

Browse source
This commit is contained in:
Leonardo de Moura 2019-11-10 18:33:31 -08:00
parent 269ae853b8
commit bd1b1af781
1 changed files with 4 additions and 7 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

11
library/Init/Lean/Meta/FunInfo.lean
View file

@ -55,11 +55,10 @@ else
@[specialize] def getFunInfoAuxAux
(whnf : Expr → MetaM Expr)
(inferType : Expr → MetaM Expr)
(fn : Expr) (maxArgs? : Option Nat) : MetaM FunInfo :=
checkFunInfoCache fn maxArgs? $ do
fnType ← inferType fn;
forallBoundedTelescope whnf fnType maxArgs? $ fun fvars type => do
fnType ← inferTypeAux whnf fn;
forallBoundedTelescope (fun e => usingTransparency TransparencyMode.all $ whnf e) fnType maxArgs? $ fun fvars type => do
pinfo ← fvars.size.foldM
(fun (i : Nat) (pinfo : Array ParamInfo) => do
let fvar := fvars.get! i;
@ -79,15 +78,13 @@ checkFunInfoCache fn maxArgs? $ do
@[inline] def getFunInfoAux
(whnf : Expr → MetaM Expr)
(inferType : Expr → MetaM Expr)
(fn : Expr) : MetaM FunInfo :=
getFunInfoAuxAux whnf inferType fn none
getFunInfoAuxAux whnf fn none
@[inline] def getFunInfoNArgsAux
(whnf : Expr → MetaM Expr)
(inferType : Expr → MetaM Expr)
(fn : Expr) (nargs : Nat) : MetaM FunInfo :=
getFunInfoAuxAux whnf inferType fn (some nargs)
getFunInfoAuxAux whnf fn (some nargs)
end Meta
end Lean