mirror of
https://github.com/leanprover/lean4.git
synced 2026-03-17 18:34:06 +00:00
08eb78a5b2
This PR sets up the new integrated test/bench suite. It then migrates all benchmarks and some related tests to the new suite. There's also some documentation and some linting. For now, a lot of the old tests are left alone so this PR doesn't become even larger than it already is. Eventually, all tests should be migrated to the new suite though so there isn't a confusing mix of two systems.
38 lines
2.8 KiB
Plaintext
38 lines
2.8 KiB
Plaintext
univInference.lean:25:48-25:54: warning: Inferred universe level for type may be unnecessarily high. The inferred resulting universe is
|
|
Type (max u v)
|
|
but it possibly could be
|
|
Sort (max (max 1 u) v)
|
|
Explicitly providing a resulting universe with no metavariables will silence this warning.
|
|
|
|
Note: The elaborated resulting universe after constructor elaboration is
|
|
Type ?u
|
|
The inference algorithm attempts to compute the smallest level for `?u` such that all universe constraints for all constructor fields are satisfied, with some approximations. The following derived constraint(s) are the cause of this possible unnecessarily high universe:
|
|
v ≤ ?u+1
|
|
u ≤ ?u+1
|
|
For example, if the resulting universe is of the form `Sort (?r + 1)` and a constructor field is in universe `Sort u`, the constraint `u ≤ ?r + 1` leads to the unnecessarily high resulting universe `Sort (u + 1)`. Using `Sort (max 1 u)` avoids this universe bump, if using it is possible.
|
|
S6 : Sort (max w₁ w₂) → Type w₂ → Sort (max w₁ (w₂ + 1))
|
|
univInference.lean:45:48-45:62: error: Invalid universe polymorphic resulting type: The resulting universe is not `Prop`, but it may be `Prop` for some parameter values:
|
|
Sort (max u v)
|
|
|
|
Hint: A possible solution is to use levels of the form `max 1 _` or `_ + 1` to ensure the universe is of the form `Type _`
|
|
univInference.lean:64:48-64:54: warning: Inferred universe level for type may be unnecessarily high. The inferred resulting universe is
|
|
Type (max u v)
|
|
but it possibly could be
|
|
Sort (max (max 1 u) v)
|
|
Explicitly providing a resulting universe with no metavariables will silence this warning.
|
|
|
|
Note: The elaborated resulting universe after constructor elaboration is
|
|
Type ?u
|
|
The inference algorithm attempts to compute the smallest level for `?u` such that all universe constraints for all constructor fields are satisfied, with some approximations. The following derived constraint(s) are the cause of this possible unnecessarily high universe:
|
|
v ≤ ?u+1
|
|
u ≤ ?u+1
|
|
For example, if the resulting universe is of the form `Sort (?r + 1)` and a constructor field is in universe `Sort u`, the constraint `u ≤ ?r + 1` leads to the unnecessarily high resulting universe `Sort (u + 1)`. Using `Sort (max 1 u)` avoids this universe bump, if using it is possible.
|
|
univInference.lean:73:48-73:62: error: Invalid universe polymorphic resulting type: The resulting universe is not `Prop`, but it may be `Prop` for some parameter values:
|
|
Sort (max u v)
|
|
|
|
Hint: A possible solution is to use levels of the form `max 1 _` or `_ + 1` to ensure the universe is of the form `Type _`
|
|
univInference.lean:94:7-94:13: error: Failed to infer universe levels in type of field `t1`
|
|
Sort ?u
|
|
univInference.lean:136:7-136:8: error: Failed to infer universe levels in type of binder `b`
|
|
sorry
|