a19ff61e15
This PR adds support for `structure` in `mutual` blocks, allowing inductive types defined by `inductive` and `structure` to be mutually recursive. The limitations are (1) that the parents in the `extends` clause must be defined before the `mutual` block and (2) mutually recursive classes are not allowed (a limitation shared by `class inductive`). There are also improvements to universe level inference for inductive types and structures. Breaking change: structure parents now elaborate with the structure in scope (fix: use qualified names or rename the structure to avoid shadowing), and structure parents no longer elaborate with autoimplicits enabled. Internally, this is a large refactor of both the `inductive` and `structure` commands. Common material is now in `Lean.Elab.MutualInductive`, and each command plugs into this mutual inductive elaboration framework with the logic specific to the respective command. For example, `structure` has code to add projections after the inductive types are added to the environment. Closes #4182
29 lines
1.8 KiB
Text
29 lines
1.8 KiB
Text
inductive1.lean:4:15-4:18: error: invalid resulting type, expecting 'Sort _' or an indexed family of sorts
|
|
inductive1.lean:12:0-12:19: error: invalid mutually inductive types, resulting universe mismatch, given
|
|
Type
|
|
expected type
|
|
Prop
|
|
inductive1.lean:22:0-22:37: error: invalid mutually inductive types, resulting universe mismatch, given
|
|
Type v
|
|
expected type
|
|
Type u
|
|
inductive1.lean:31:0-31:41: error: invalid mutually inductive types, parameter 'x' has type
|
|
Bool : Type
|
|
but is expected to have type
|
|
Nat : Type
|
|
inductive1.lean:40:0-40:30: error: invalid inductive type, number of parameters mismatch in mutually inductive datatypes
|
|
inductive1.lean:49:0-49:40: error: invalid mutually inductive types, binder annotation mismatch at parameter 'x'
|
|
inductive1.lean:59:0-59:45: error: invalid inductive type, universe parameters mismatch in mutually inductive datatypes
|
|
inductive1.lean:69:2-69:5: error: 'Boo.T1.bla' has already been declared
|
|
inductive1.lean:73:10-73:12: error: 'Boo.T1' has already been declared
|
|
inductive1.lean:80:0-80:27: error: invalid use of 'partial' in inductive declaration
|
|
inductive1.lean:81:0-81:33: error: invalid use of 'noncomputable' in inductive declaration
|
|
inductive1.lean:82:2-82:8: error: declaration is not a definition 'T1''
|
|
inductive1.lean:85:0-85:17: error: invalid 'private' constructor in a 'private' inductive datatype
|
|
inductive1.lean:93:7-93:26: error: invalid inductive type, cannot mix unsafe and safe declarations in a mutually inductive datatypes
|
|
inductive1.lean:100:0-100:4: error: constructor resulting type must be specified in inductive family declaration
|
|
inductive1.lean:105:7-105:9: error: type expected, got
|
|
(T1 : Nat → Type)
|
|
inductive1.lean:108:0-108:10: error: unexpected constructor resulting type
|
|
Nat
|
|
inductive1.lean:118:7-118:11: error: unknown identifier 'cons'
|