27b583d304
This PR changes the elaboration of the `structure`/`class` commands so that default values have later fields in context as well. This allows field defaults to depend on fields that come both before and after them. While this was already the case for inherited fields to some degree, it now applies uniformly to all fields. Additionally, when elaborating the default value for a field, all fields that depend on it are cleared from the context to avoid situations where the default value depends on itself. This addresses an issue reported by Aaron Liu [on Zulip](https://leanprover.zulipchat.com/#narrow/channel/270676-lean4/topic/default.20structure.20values.20can.20depend.20on.20themselves/near/578014370).
57 lines
1.1 KiB
Text
57 lines
1.1 KiB
Text
--
|
||
|
||
structure A (α : Type) where
|
||
(x : α)
|
||
|
||
structure B (α : Type) where
|
||
(x : α)
|
||
|
||
structure S : Nat where -- error expected Type
|
||
(x : Nat)
|
||
|
||
structure S extends Nat → Nat where -- error expected structure
|
||
(x : Nat)
|
||
set_option structureDiamondWarning true in
|
||
structure S' extends A Nat, B Nat where -- error field `x` already declared
|
||
(x : Nat)
|
||
structure SDup extends A Nat, A Nat where -- duplicate parent structure 'A'
|
||
|
||
structure S extends A Nat, B Bool where -- error field `x` from `B` has already been declared
|
||
(x : Nat)
|
||
|
||
structure S1 where
|
||
(_x : Nat)
|
||
|
||
structure S2 where
|
||
(x _y : Nat)
|
||
|
||
structure S where
|
||
(x : Nat)
|
||
(x : Nat) -- error
|
||
|
||
structure S extends A Nat where
|
||
(x : Nat) -- error
|
||
|
||
structure S' extends A Nat where
|
||
(x := true) -- error type mismatch
|
||
|
||
structure S extends A Nat where
|
||
(x : Bool := true) -- error type mismatch
|
||
|
||
structure S'' where
|
||
(x : Nat := true) -- error type mismatch
|
||
|
||
private structure Spriv where
|
||
private mk :: (x : Nat)
|
||
|
||
private structure Spriv where
|
||
protected mk :: (x : Nat)
|
||
|
||
private structure Spriv where
|
||
protected (x : Nat)
|
||
|
||
private structure Spriv where
|
||
mk2 :: (x : Nat)
|
||
|
||
#check Spriv
|
||
#check S.mk2
|