max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

doc: fix typos around inductiveCheckResultingUniverse (#3309)

Browse source 
The unpaired backtick was causing weird formatting in vscode doc hovers.

Also closes an unpaired `(` in an error message.
This commit is contained in:
Eric Wieser 2024-02-12 10:11:50 +00:00 • committed by GitHub
parent 90b08ef22e
commit 1965a022eb
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
2 changed files with 5 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/Lean/Elab/Inductive.lean
View file

@ -524,14 +524,14 @@ private def updateResultingUniverse (views : Array InductiveView) (numParams : N
register_builtin_option bootstrap.inductiveCheckResultingUniverse : Bool := {
defValue := true,
group := "bootstrap",
descr := "by default the `inductive/structure commands report an error if the resulting universe is not zero, but may be zero for some universe parameters. Reason: unless this type is a subsingleton, it is hardly what the user wants since it can only eliminate into `Prop`. In the `Init` package, we define subsingletons, and we use this option to disable the check. This option may be deleted in the future after we improve the validator"
descr := "by default the `inductive`/`structure` commands report an error if the resulting universe is not zero, but may be zero for some universe parameters. Reason: unless this type is a subsingleton, it is hardly what the user wants since it can only eliminate into `Prop`. In the `Init` package, we define subsingletons, and we use this option to disable the check. This option may be deleted in the future after we improve the validator"
}
def checkResultingUniverse (u : Level) : TermElabM Unit := do
if bootstrap.inductiveCheckResultingUniverse.get (← getOptions) then
let u ← instantiateLevelMVars u
if !u.isZero && !u.isNeverZero then
throwError "invalid universe polymorphic type, the resultant universe is not Prop (i.e., 0), but it may be Prop for some parameter values (solution: use 'u+1' or 'max 1 u'{indentD u}"
throwError "invalid universe polymorphic type, the resultant universe is not Prop (i.e., 0), but it may be Prop for some parameter values (solution: use 'u+1' or 'max 1 u'){indentD u}"
private def checkResultingUniverses (views : Array InductiveView) (numParams : Nat) (indTypes : List InductiveType) : TermElabM Unit := do
let u := (← instantiateLevelMVars (← getResultingUniverse indTypes)).normalize

6
tests/lean/univInference.lean.expected.out
View file

@ -4,7 +4,7 @@ structure resulting type
Type ?u
recall that Lean only infers the resulting universe level automatically when there is a unique solution for the universe level constraints, consider explicitly providing the structure resulting universe level
S6 : Sort (max w₁ w₂) → Type w₂ → Sort (max w₁ (w₂ + 1))
univInference.lean:45:0-46:17: error: invalid universe polymorphic type, the resultant universe is not Prop (i.e., 0), but it may be Prop for some parameter values (solution: use 'u+1' or 'max 1 u'
univInference.lean:45:0-46:17: error: invalid universe polymorphic type, the resultant universe is not Prop (i.e., 0), but it may be Prop for some parameter values (solution: use 'u+1' or 'max 1 u')
max u v
univInference.lean:65:2-65:22: error: failed to compute resulting universe level of inductive datatype, constructor 'Induct.S4.mk' has type
{α : Sort u} → {β : Sort v} → α → β → S4 α β
@ -13,7 +13,7 @@ parameter 'a' has type
inductive type resulting type
Type ?u
recall that Lean only infers the resulting universe level automatically when there is a unique solution for the universe level constraints, consider explicitly providing the inductive type resulting universe level
univInference.lean:73:0-74:22: error: invalid universe polymorphic type, the resultant universe is not Prop (i.e., 0), but it may be Prop for some parameter values (solution: use 'u+1' or 'max 1 u'
univInference.lean:73:0-74:22: error: invalid universe polymorphic type, the resultant universe is not Prop (i.e., 0), but it may be Prop for some parameter values (solution: use 'u+1' or 'max 1 u')
max u v
univInference.lean:81:0-82:22: error: invalid universe polymorphic type, the resultant universe is not Prop (i.e., 0), but it may be Prop for some parameter values (solution: use 'u+1' or 'max 1 u'
univInference.lean:81:0-82:22: error: invalid universe polymorphic type, the resultant universe is not Prop (i.e., 0), but it may be Prop for some parameter values (solution: use 'u+1' or 'max 1 u')
max u v