Skip to content

Commit 6703d75

Browse files
doc: fix typo in Init.Coe module docstring
1 parent 2fff4c6 commit 6703d75

File tree

1 file changed

+1
-1
lines changed

1 file changed

+1
-1
lines changed

src/Init/Coe.lean

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -116,7 +116,7 @@ On top of these instances this file defines several auxiliary type classes:
116116
* `CoeOTC := CoeOut* Coe*`
117117
* `CoeHTC := CoeHead? CoeOut* Coe*`
118118
* `CoeHTCT := CoeHead? CoeOut* Coe* CoeTail?`
119-
* `CoeDep := CoeHead? CoeOut* Coe* CoeTail? | CoeDep`
119+
* `CoeT := CoeHead? CoeOut* Coe* CoeTail? | CoeDep`
120120
121121
-/
122122

0 commit comments

Comments
 (0)