| univInference.lean:25:0-27:9: error: failed to compute resulting universe level of structure, field 'Struct.S4.a' has type | |
| α : Sort u | |
| 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') | |
| 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 α β | |
| parameter 'a' has type | |
| α : Sort u | |
| 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') | |
| 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') | |
| max u v |