diff options
Diffstat (limited to 'tests/examplefiles')
| -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 |