Skip to content

Commit 9b0aedc

Browse files
committed
Auto merge of #699 - spastorino:fold-depth-example, r=jackh726
Add Fold binders depth example
2 parents 7148968 + 10f5f51 commit 9b0aedc

File tree

1 file changed

+8
-2
lines changed

1 file changed

+8
-2
lines changed

book/src/types/operations/fold.md

Lines changed: 8 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -62,8 +62,14 @@ Each callback in the [`Folder`] trait takes a `binders` argument. This indicates
6262
the number of binders that we have traversed during folding, which is relevant for De Bruijn indices.
6363
So e.g. a bound variable with depth 1, if invoked with a `binders` value of 1, indicates something that was bound to something external to the fold.
6464

65-
XXX explain with examples and in more detail
66-
65+
For example, consider:
66+
67+
```rust,ignore
68+
Foo<'a>: for<'b> Bar<'b>
69+
```
70+
71+
In this case, `Foo<'a>` gets visited with depth 0 and `Bar<'b>` gets visited with depth 1.
72+
6773
## The `Fold::Result` associated type
6874

6975
The `Fold` trait defines a [`Result`] associated type, indicating the

0 commit comments

Comments
 (0)