• Léon Gondelman's avatar
    Just a sketch of a very naive vcgen for heap-lang, · c36dda2a
    Léon Gondelman authored
    without any optimisation.
    Next steps:
     modify definition of wp_expr, with a deep embedding of
      - functions : to allow optimisation go recursively through lambdas,
        in particular, to allow exhale-inhale optimisation;
      - conjunction and equations : to allow optimisation
        of redundant and trivial equations
_CoqProject 452 Bytes