diff options
| author | Eric Wieser <wieser.eric@gmail.com> | 2023-04-20 14:10:50 +0100 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2023-04-20 15:10:50 +0200 |
| commit | d5bfdd4cca547fa3e14dea6e89a29be8019efdf5 (patch) | |
| tree | 7b4365a2af82e605ddd7d0229171a747bf5eb5b5 /tests | |
| parent | 50207e008d92f7a8750a8d080863e5cada0b0fca (diff) | |
| download | pygments-git-d5bfdd4cca547fa3e14dea6e89a29be8019efdf5.tar.gz | |
lean: correctly parse expressions nested within attributes (#1817)
Diffstat (limited to 'tests')
| -rw-r--r-- | tests/examplefiles/lean/test.lean | 4 | ||||
| -rw-r--r-- | tests/examplefiles/lean/test.lean.output | 25 |
2 files changed, 29 insertions, 0 deletions
diff --git a/tests/examplefiles/lean/test.lean b/tests/examplefiles/lean/test.lean index 2c8b1358..4b719e13 100644 --- a/tests/examplefiles/lean/test.lean +++ b/tests/examplefiles/lean/test.lean @@ -207,3 +207,7 @@ let ⟨m, hm⟩ := @zorn α (≤) h (assume a b c, le_trans) in ⟨m, assume a ha, le_antisymm (hm a ha) ha⟩ end zorn + +-- other bits of tricky syntax +@[to_additive "See note [foo]"] +lemma mul_one : sorry := sorry diff --git a/tests/examplefiles/lean/test.lean.output b/tests/examplefiles/lean/test.lean.output index 2a258da8..dd144778 100644 --- a/tests/examplefiles/lean/test.lean.output +++ b/tests/examplefiles/lean/test.lean.output @@ -3604,4 +3604,29 @@ 'end' Keyword.Declaration ' ' Text 'zorn' Name +'\n\n' Text + +'-- other bits of tricky syntax' Comment.Single +'\n' Text + +'@[' Keyword.Declaration +'to_additive' Name +' ' Text +'"' Literal.String.Double +'See note [foo]' Literal.String.Double +'"' Literal.String.Double +']' Keyword.Declaration +'\n' Text + +'lemma' Keyword.Declaration +' ' Text +'mul_one' Name +' ' Text +':' Operator +' ' Text +'sorry' Generic.Error +' ' Text +':=' Operator +' ' Text +'sorry' Generic.Error '\n' Text |