Skip to content

Commit dab3483

Browse files
authored
doc: clarify what checks honest library authors must do (#849)
The previous phrasing "[that they performed this check](https://github.com/leanprover/reference-manual/blob/main/Manual/ValidatingProofs.lean#L67C188-L67C207)" was ambiguous. The new phrasing explicitly states who should do what check. Closes #848
1 parent 8ae381a commit dab3483

1 file changed

Lines changed: 1 addition & 1 deletion

File tree

Manual/ValidatingProofs.lean

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -64,7 +64,7 @@ The blue ticks indicate that the theorem statement has been successfully elabora
6464

6565
## Trust
6666

67-
This check is meaningful if one believes the formal theorem statement corresponds to its intended informal meanings and trusts the authors of the imported libraries to be {tech}[honest], that they performed this check, and that no unsound axioms have been declared and used.
67+
This check is meaningful if one believes the formal theorem statement corresponds to its intended informal meanings and trusts the authors of the imported libraries to be {tech}[honest], that they checked that the theorems in their libraries express their intended informal meanings, and that no unsound axioms have been declared and used.
6868

6969
## Protection
7070

0 commit comments

Comments
 (0)