From a88dca17bc401c4b5bad7842b27b57ae02e3bb95 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 14 Jan 2020 08:51:50 -0800 Subject: [PATCH] chore: style --- src/Init/Lean/Meta/SynthInstance.lean | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/src/Init/Lean/Meta/SynthInstance.lean b/src/Init/Lean/Meta/SynthInstance.lean index 660eee2e48..fe6213328c 100644 --- a/src/Init/Lean/Meta/SynthInstance.lean +++ b/src/Init/Lean/Meta/SynthInstance.lean @@ -231,15 +231,16 @@ withMCtx mctx $ do mvarType ← instantiateMVars mvarType; pure $ mkTableKey mctx mvarType -/- See `getSubgoals` +/- See `getSubgoals` and `getSubgoalsAux` We use the parameter `j` to reduce the number of `instantiate*` invocations. It is the same approach we use at `forallTelescope` and `lambdaTelescope`. Given `getSubgoalsAux args j subgoals instVal type`, we have that `type.instantiateRevRange j args.size args` does not have loose bound variables. -/ structure SubgoalsResult : Type := -(subgoals : List Expr) -(instVal instTypeBody : Expr) +(subgoals : List Expr) +(instVal : Expr) +(instTypeBody : Expr) private partial def getSubgoalsAux (lctx : LocalContext) (localInsts : LocalInstances) (xs : Array Expr) : Array Expr → Nat → List Expr → Expr → Expr → MetaM SubgoalsResult