Skip to content

Commit 58e8015

Browse files
fix: clarify structure inheritance (#254)
1 parent ca74c30 commit 58e8015

File tree

1 file changed

+2
-1
lines changed

1 file changed

+2
-1
lines changed

Manual/Language/InductiveTypes/Structures.lean

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -341,7 +341,8 @@ deriving Repr
341341

342342
When the new structure extends existing structures, the new structure's constructor takes the existing structure's information as additional arguments.
343343
Typically, this is in the form of a constructor parameter for each parent structure type.
344-
If the parents' fields overlap, however, then the subset of non-overlapping fields from one or more of the parents is included instead to prevent duplicating field information.
344+
This parent value contains all of the parent's fields.
345+
If the parents' fields overlap, however, then the subset of non-overlapping fields from one or more of the parents is included instead of an entire value of the parent structure to prevent duplicating field information.
345346

346347

347348
There is no subtyping relation between a parent structure type and its children.

0 commit comments

Comments
 (0)