Skip to content

Commit

Permalink
Unmark second block as Rzk to prevent a type error
Browse files Browse the repository at this point in the history
Because otherwise the identifier `id` would be a duplicate
  • Loading branch information
aabounegm committed Jan 9, 2024
1 parent da09c33 commit e8bee72
Showing 1 changed file with 2 additions and 2 deletions.
4 changes: 2 additions & 2 deletions docs/docs/en/posts/2023-12-24-formatter.rzk.md
Original file line number Diff line number Diff line change
Expand Up @@ -45,9 +45,9 @@ For example, consider the following Rzk code:
#define id (A : U) (x : A) : A := x
```
which has 11 positions where a new line can be inserted, as shown by these markers:
```rzk
```
#define id (A : U) (x : A) : A := x
-- ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^
^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^
```
This amounts to 2048 combinations that have to be ranked for such a simple line.
Even the ranking itself is not a straightforward problem to tackle.
Expand Down

0 comments on commit e8bee72

Please sign in to comment.