From 0ad611cf2ff01243c911e90740e627e028b60c87 Mon Sep 17 00:00:00 2001 From: Marcus Rossel Date: Thu, 30 Nov 2023 11:16:33 +0100 Subject: [PATCH] doc: fix typos (#2996) --- src/Lean/Expr.lean | 6 +++--- src/Lean/Meta/CollectMVars.lean | 4 ++-- 2 files changed, 5 insertions(+), 5 deletions(-) diff --git a/src/Lean/Expr.lean b/src/Lean/Expr.lean index 63bdd45d97..0523ac984c 100644 --- a/src/Lean/Expr.lean +++ b/src/Lean/Expr.lean @@ -774,8 +774,8 @@ instance : BEq Expr where beq := Expr.eqv /-- -Return true iff `a` and `b` are equal. -Binder names and annotations are taking into account. +Return `true` iff `a` and `b` are equal. +Binder names and annotations are taken into account. -/ @[extern "lean_expr_equal"] opaque equal (a : @& Expr) (b : @& Expr) : Bool @@ -831,7 +831,7 @@ def isConst : Expr → Bool | _ => false /-- -Return `true` if the given expression is a constant of the give name. +Return `true` if the given expression is a constant of the given name. Examples: - `` (.const `Nat []).isConstOf `Nat `` is `true` - `` (.const `Nat []).isConstOf `False `` is `false` diff --git a/src/Lean/Meta/CollectMVars.lean b/src/Lean/Meta/CollectMVars.lean index 728deccccd..bcde280f49 100644 --- a/src/Lean/Meta/CollectMVars.lean +++ b/src/Lean/Meta/CollectMVars.lean @@ -28,12 +28,12 @@ partial def collectMVars (e : Expr) : StateRefT CollectMVars.State MetaM Unit := | none => pure () | some d => collectMVars (mkMVar d.mvarIdPending) -/-- Return metavariables in occurring the given expression. See `collectMVars` -/ +/-- Return metavariables occurring in the given expression. See `collectMVars` -/ def getMVars (e : Expr) : MetaM (Array MVarId) := do let (_, s) ← (collectMVars e).run {} pure s.result -/-- Similar to getMVars, but removes delayed assignments. -/ +/-- Similar to `getMVars`, but removes delayed assignments. -/ def getMVarsNoDelayed (e : Expr) : MetaM (Array MVarId) := do let mvarIds ← getMVars e mvarIds.filterM fun mvarId => not <$> mvarId.isDelayedAssigned