search

creusot-rs / creusot

Creusot helps you prove your code is correct in an automated fashion.
GNU Lesser General Public License v2.1
1.12k stars 50 forks source link

Allow usage of `proof_assert` in closures #1106

Closed arnaudgolfouse closed 1 week ago

arnaudgolfouse commented 1 week ago

Should fix #1072

arnaudgolfouse commented 1 week ago

The place_to_term function is not ideal, and should probably be merged with util::ClosureSubst ?

jhjourdan commented 1 week ago

Could you add some tests?

arnaudgolfouse commented 1 week ago

Could you add some tests?

I added some very basic tests, if you have a more complicated idea in mind don't hesitate

jhjourdan commented 1 week ago

I'm not asking anything complicated. Jsut a basic test to check that this feature still works in the future.

jhjourdan commented 1 week ago

This looks good. Let's merge.

arnaudgolfouse commented 1 week ago

Why is list_reversal_lasso failing? It seems to be unrelated, and it passes on my machine...

jhjourdan commented 1 week ago

Is it failing? If the PR has been mergend, this means that it has succeeded.