search

delcypher / freeboogie

Automatically exported from code.google.com/p/freeboogie
0 stars 1 forks source link

desugar function bodies #36

Open GoogleCodeExporter opened 9 years ago

GoogleCodeExporter commented 9 years ago 
The code
  function f(args) returns (results) { expr }
is equivalent to
  function f(args) returns (results);
  axiom (forall args, results :: f(args) == expr);

Do the desugaring.

Original issue reported on code.google.com by radugrig...@gmail.com on 26 Aug 2009 at 2:36