diff options
| author | Emilio Jesus Gallego Arias | 2020-03-04 16:37:49 -0500 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-08-27 19:03:33 +0200 |
| commit | 3fcd90f590bf0b40e24e20d18f96776232cb014e (patch) | |
| tree | dfd40f571482b0acd0b468be815e08e0602678a7 /plugins/syntax | |
| parent | 094e4649c29e2426daca0476c140439de901dafe (diff) | |
[zarith] [notation] Build less intermediate values
We could still optimize the functions in that file a bit more if there
is need.
Diffstat (limited to 'plugins/syntax')
0 files changed, 0 insertions, 0 deletions