Testing linearity

Stream: lean4

[François G. Dorais]

I would like to check that a certain function uses a certain parameter linearly: basically that refcounts related to that parameter are always the same going in and going out. How can I do that? (Without inspecting the code manually, which is error prone.)

[Mario Carneiro]

currently, there is no alternative to checking the IR

[Mario Carneiro]

or profiling