aboutsummaryrefslogtreecommitdiff
path: root/doc/plugin_tutorial/tuto2/src/persistent_counter.mli
diff options
context:
space:
mode:
authorEmilio Jesus Gallego Arias2020-03-04 16:37:49 -0500
committerEmilio Jesus Gallego Arias2020-08-27 19:03:33 +0200
commit3fcd90f590bf0b40e24e20d18f96776232cb014e (patch)
treedfd40f571482b0acd0b468be815e08e0602678a7 /doc/plugin_tutorial/tuto2/src/persistent_counter.mli
parent094e4649c29e2426daca0476c140439de901dafe (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 'doc/plugin_tutorial/tuto2/src/persistent_counter.mli')
0 files changed, 0 insertions, 0 deletions