From 2eb44b3cdc41888549e8e73fcaa4e76d1ac43a6a Mon Sep 17 00:00:00 2001 From: Sebastian Graf Date: Tue, 21 Oct 2025 11:07:24 +0200 Subject: [PATCH] chore: fix a typo in the docstring for `SeqRight` and add documentation to `getLevel` (#10866) --- src/Init/Prelude.lean | 2 +- src/Lean/Meta/InferType.lean | 6 ++++++ 2 files changed, 7 insertions(+), 1 deletion(-) diff --git a/src/Init/Prelude.lean b/src/Init/Prelude.lean index 0098fb5b55..951ab37a10 100644 --- a/src/Init/Prelude.lean +++ b/src/Init/Prelude.lean @@ -3703,7 +3703,7 @@ When thinking about `f` as potential side effects, `*>` evaluates first the left argument for their side effects, discarding the value of the left argument and returning the value of the right argument. -For most applications, `Applicative` or `Monad` should be used rather than `SeqLeft` itself. +For most applications, `Applicative` or `Monad` should be used rather than `SeqRight` itself. -/ class SeqRight (f : Type u → Type v) : Type (max (u+1) v) where /-- diff --git a/src/Lean/Meta/InferType.lean b/src/Lean/Meta/InferType.lean index 11fd5413ca..e48df2178b 100644 --- a/src/Lean/Meta/InferType.lean +++ b/src/Lean/Meta/InferType.lean @@ -129,6 +129,12 @@ private def inferProjType (structName : Name) (idx : Nat) (e : Expr) : MetaM Exp def throwTypeExpected {α} (type : Expr) : MetaM α := throwError "type expected{indentExpr type}" +/-- +If `type : sort` and `sort` reduces to `Sort u` for some `u`, then `getLevel type` returns `u`. + +If `sort` is an assignable MVar, then `getLevel type` produces a fresh level metavariable `?u`, +assigns the MVar to `Sort ?u` and returns `?u`. +-/ def getLevel (type : Expr) : MetaM Level := do let typeType ← inferType type let typeType ← whnfD typeType