From 4ec1c10dc08caed81ec80fcd971bc8ab2e48559c Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 16 Jan 2023 07:54:20 -0800 Subject: [PATCH] chore: comments at private function `mkAuxMVarType` --- src/Lean/MetavarContext.lean | 12 +++--------- 1 file changed, 3 insertions(+), 9 deletions(-) diff --git a/src/Lean/MetavarContext.lean b/src/Lean/MetavarContext.lean index 944edf3708..decc9dd73d 100644 --- a/src/Lean/MetavarContext.lean +++ b/src/Lean/MetavarContext.lean @@ -1023,10 +1023,9 @@ mutual /-- Given a metavariable with type `e`, kind `kind` and free/meta variables `xs` in its local context `lctx`, - get the type of the corresponding auxiliary metavariable. - This follows the pattern of pi-abstracting the types of `xs` in reverse order, - with the exception of non-`syntheticOpaque` let-bound free variables - (see "Gruesome details" section in the beginning of the file). + create the type for a new auxiliary metavariable. These auxiliary metavariables are created by `elimMVar`. + + See "Gruesome details" section in the beginning of the file. Note: It is assumed that `xs` is the result of calling `collectForwardDeps` on a subset of variables in `lctx`. -/ @@ -1059,11 +1058,6 @@ mutual let id ← if mvarDecl.userName.isAnonymous then mkFreshBinderName else pure mvarDecl.userName return Lean.mkForall id (← read).binderInfoForMVars type e where - /-- Helper function that must be called on any expression that will be - included in the type of the auxiliary metavar. Given an expression `e`, it will: - 1. Recursively eliminate `xs` from the contexts of any metavariables that appear within `e`. - 2. Immediately replace the occurrences of `xs` with bound variables so that none appear - in the resulting type of the metavar (where `xs` will be stripped from the local context). -/ abstractRangeAux (xs : Array Expr) (i : Nat) (e : Expr) : M Expr := do let e ← elim xs e pure (e.abstractRange i xs)