From da71dd3d773574fc3daa9448f45c2b4b50940f4b Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 18 Jul 2022 11:41:53 -0400 Subject: [PATCH] chore: docstring --- src/Lean/Meta/Basic.lean | 24 ++++++++++++------------ 1 file changed, 12 insertions(+), 12 deletions(-) diff --git a/src/Lean/Meta/Basic.lean b/src/Lean/Meta/Basic.lean index b36adf4c65..33e997bd59 100644 --- a/src/Lean/Meta/Basic.lean +++ b/src/Lean/Meta/Basic.lean @@ -34,22 +34,22 @@ namespace Lean.Meta builtin_initialize isDefEqStuckExceptionId : InternalExceptionId ← registerInternalExceptionId `isDefEqStuck /-- - Configuration flags for the `MetaM` monad. - Many of them are used to control the `isDefEq` function that checks whether two terms are definitionally equal or not. - Recall that when `isDefEq` is trying to check whether - `?m@C a₁ ... aₙ` and `t` are definitionally equal (`?m@C a₁ ... aₙ =?= t`), where - `?m@C` as a shorthand for `C |- ?m : t` where `t` is the type of `?m`. - We solve it using the assignment `?m := fun a₁ ... aₙ => t` if - 1) `a₁ ... aₙ` are pairwise distinct free variables that are ​*not*​ let-variables. - 2) `a₁ ... aₙ` are not in `C` - 3) `t` only contains free variables in `C` and/or `{a₁, ..., aₙ}` - 4) For every metavariable `?m'@C'` occurring in `t`, `C'` is a subprefix of `C` - 5) `?m` does not occur in `t` +Configuration flags for the `MetaM` monad. +Many of them are used to control the `isDefEq` function that checks whether two terms are definitionally equal or not. +Recall that when `isDefEq` is trying to check whether +`?m@C a₁ ... aₙ` and `t` are definitionally equal (`?m@C a₁ ... aₙ =?= t`), where +`?m@C` as a shorthand for `C |- ?m : t` where `t` is the type of `?m`. +We solve it using the assignment `?m := fun a₁ ... aₙ => t` if +1) `a₁ ... aₙ` are pairwise distinct free variables that are ​*not*​ let-variables. +2) `a₁ ... aₙ` are not in `C` +3) `t` only contains free variables in `C` and/or `{a₁, ..., aₙ}` +4) For every metavariable `?m'@C'` occurring in `t`, `C'` is a subprefix of `C` +5) `?m` does not occur in `t` -/ structure Config where /-- If `foApprox` is set to true, and some `aᵢ` is not a free variable, - then we use first-order unification + then we use first-order unification ``` ?m a_1 ... a_i a_{i+1} ... a_{i+k} =?= f b_1 ... b_k ```