diff --git a/src/Init/Data/Array/Basic.lean b/src/Init/Data/Array/Basic.lean index 55ad75d8f6..17bb601808 100644 --- a/src/Init/Data/Array/Basic.lean +++ b/src/Init/Data/Array/Basic.lean @@ -559,9 +559,9 @@ def modifyOp (xs : Array α) (idx : Nat) (f : α → α) : Array α := xs.modify idx f /-- - We claim this unsafe implementation is correct because an array cannot have more than `usizeSz` elements in our runtime. + We claim this unsafe implementation is correct because an array cannot have more than `USize.size` elements in our runtime. - This kind of low level trick can be removed with a little bit of compiler support. For example, if the compiler simplifies `as.size < usizeSz` to true. -/ + This kind of low level trick can be removed with a little bit of compiler support. For example, if the compiler simplifies `as.size < USize.size` to true. -/ @[inline] unsafe def forIn'Unsafe {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (as : Array α) (b : β) (f : (a : α) → a ∈ as → β → m (ForInStep β)) : m β := let sz := as.usize let rec @[specialize] loop (i : USize) (b : β) : m β := do diff --git a/src/Init/Notation.lean b/src/Init/Notation.lean index 86e95cd066..ecfe7f13f9 100644 --- a/src/Init/Notation.lean +++ b/src/Init/Notation.lean @@ -722,7 +722,7 @@ syntax (name := runElab) "run_elab " doSeq : command /-- The `run_meta doSeq` command executes code in `MetaM Unit`. -This is the same as `#eval show MetaM Unit from do discard doSeq`. +This is the same as `#eval show MetaM Unit from discard do doSeq`. (This is effectively a synonym for `run_elab` since `MetaM` lifts to `TermElabM`.) -/ diff --git a/src/Init/Prelude.lean b/src/Init/Prelude.lean index 6b33e68b82..df1cd7e77f 100644 --- a/src/Init/Prelude.lean +++ b/src/Init/Prelude.lean @@ -4674,7 +4674,7 @@ inductive Name where /-- The "anonymous" name. -/ | anonymous : Name /-- - A string name. The name `Lean.Meta.run` is represented at + A string name. The name `Lean.Meta.run` is represented as ```lean .str (.str (.str .anonymous "Lean") "Meta") "run" ``` diff --git a/src/Lean/Expr.lean b/src/Lean/Expr.lean index 7224cbd086..9b3a71b390 100644 --- a/src/Lean/Expr.lean +++ b/src/Lean/Expr.lean @@ -253,7 +253,7 @@ instance : EmptyCollection (FVarIdMap α) := inferInstanceAs (EmptyCollection (S instance : Inhabited (FVarIdMap α) where default := {} -/-- Universe metavariable Id -/ +/-- Expression metavariable Id -/ structure MVarId where name : Name deriving Inhabited, BEq, Hashable @@ -301,8 +301,8 @@ inductive Expr where of a variable in the expression where there is a variable binder above it (i.e. introduced by a `lam`, `forallE`, or `letE`). - The `deBruijnIndex` parameter is the *de-Bruijn* index for the bound - variable. See [the Wikipedia page on de-Bruijn indices](https://en.wikipedia.org/wiki/De_Bruijn_index) + The `deBruijnIndex` parameter is the *de Bruijn* index for the bound + variable. See [the Wikipedia page on de Bruijn indices](https://en.wikipedia.org/wiki/De_Bruijn_index) for additional information. For example, consider the expression `fun x : Nat => forall y : Nat, x = y`. @@ -321,16 +321,16 @@ inductive Expr where | bvar (deBruijnIndex : Nat) /-- - The `fvar` constructor represent free variables. These *free* variable - occurrences are not bound by an earlier `lam`, `forallE`, or `letE` + The `fvar` constructor represents free variables. Such a *free* variable + occurrence is not bound by an earlier `lam`, `forallE`, or `letE` constructor and its binder exists in a local context only. - Note that Lean uses the *locally nameless approach*. See [McBride and McKinna](https://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.365.2479&rep=rep1&type=pdf) + Note that Lean uses the *locally nameless approach*. See [McBride and McKinna](https://doi.org/10.1145/1017472.1017477) for additional details. When "visiting" the body of a binding expression (i.e. `lam`, `forallE`, or `letE`), bound variables are converted into free variables using a unique identifier, - and their user-facing name, type, value (for `LetE`), and binder annotation + and their user-facing name, type, value (for `letE`), and binder annotation are stored in the `LocalContext`. -/ | fvar (fvarId : FVarId) @@ -363,7 +363,7 @@ inductive Expr where A function application. For example, the natural number one, i.e. `Nat.succ Nat.zero` is represented as - ``Expr.app (.const `Nat.succ []) (.const .zero [])``. + ``Expr.app (.const `Nat.succ []) (.const `Nat.zero [])``. Note that multiple arguments are represented using partial application. For example, the two argument application `f x y` is represented as @@ -383,7 +383,7 @@ inductive Expr where | lam (binderName : Name) (binderType : Expr) (body : Expr) (binderInfo : BinderInfo) /-- - A dependent arrow `(a : α) → β)` (aka forall-expression) where `β` may dependent + A dependent arrow `(a : α) → β)` (aka forall-expression) where `β` may depend on `a`. Note that this constructor is also used to represent non-dependent arrows where `β` does not depend on `a`. diff --git a/src/Lean/Meta/Tactic/Util.lean b/src/Lean/Meta/Tactic/Util.lean index d085c40a6f..b583d6d0da 100644 --- a/src/Lean/Meta/Tactic/Util.lean +++ b/src/Lean/Meta/Tactic/Util.lean @@ -68,11 +68,11 @@ def _root_.Lean.MVarId.checkNotAssigned (mvarId : MVarId) (tacticName : Name) : ++ .note "This likely indicates an internal error in this tactic or a prior one" throwTacticEx tacticName mvarId msg -/-- Get the type the given metavariable. -/ +/-- Get the type of the given metavariable. -/ def _root_.Lean.MVarId.getType (mvarId : MVarId) : MetaM Expr := return (← mvarId.getDecl).type -/-- Get the type the given metavariable after instantiating metavariables and reducing to +/-- Get the type of the given metavariable after instantiating metavariables and reducing to weak head normal form. -/ -- The `instantiateMVars` needs to be on the outside, -- since `whnf` can unfold local definitions which may introduce metavariables. diff --git a/src/Lean/MetavarContext.lean b/src/Lean/MetavarContext.lean index 137bfbb085..0c95664f56 100644 --- a/src/Lean/MetavarContext.lean +++ b/src/Lean/MetavarContext.lean @@ -510,7 +510,7 @@ def hasAssignableMVar [Monad m] [MonadMCtx m] : Expr → m Bool /-- Add `mvarId := u` to the universe metavariable assignment. - This method does not check whether `mvarId` is already assigned, nor it checks whether + This method does not check whether `mvarId` is already assigned, nor does it check whether a cycle is being introduced. This is a low-level API, and it is safer to use `isLevelDefEq (mkLevelMVar mvarId) u`. -/ @@ -523,7 +523,7 @@ def assignLevelMVarExp (m : MetavarContext) (mvarId : LMVarId) (val : Level) : M /-- Add `mvarId := x` to the metavariable assignment. -This method does not check whether `mvarId` is already assigned, nor it checks whether +This method does not check whether `mvarId` is already assigned, nor does it check whether a cycle is being introduced, or whether the expression has the right type. This is a low-level API, and it is safer to use `isDefEq (mkMVar mvarId) x`. -/ diff --git a/src/Std/Data/HashMap/Raw.lean b/src/Std/Data/HashMap/Raw.lean index 48b60d460e..3b6d0d1286 100644 --- a/src/Std/Data/HashMap/Raw.lean +++ b/src/Std/Data/HashMap/Raw.lean @@ -16,7 +16,7 @@ set_option autoImplicit false /-! # Hash maps with unbundled well-formedness invariant -This module develops the type `Std.HashMap.Raw` of dependent hash maps with unbundled +This module develops the type `Std.HashMap.Raw` of hash maps with unbundled well-formedness invariant. This version is safe to use in nested inductive types. The well-formedness predicate is diff --git a/tests/elab/Reparen.lean.out.expected b/tests/elab/Reparen.lean.out.expected index f3feac0b4c..d844206b02 100644 --- a/tests/elab/Reparen.lean.out.expected +++ b/tests/elab/Reparen.lean.out.expected @@ -4620,7 +4620,7 @@ inductive Name where /-- The "anonymous" name. -/ | anonymous : Name /-- - A string name. The name `Lean.Meta.run` is represented at + A string name. The name `Lean.Meta.run` is represented as ```lean .str (.str (.str .anonymous "Lean") "Meta") "run" ```