Another example for eHoare#845

Open

namasikanam wants to merge 26 commits intomainfrom

eHoare-example

Commits on Jan 30, 2026

Documentation comments and corresponding HTML generation.

MM45
authored and
namasikanam
committed
fix handling of bounds in conseq equiv phoare

oskgo
authored and
namasikanam
committed
add manual trivial application to conseq variant (#848)

oskgo
authored and
namasikanam
committed
reduce when needed in proc and call rules (#849)

bgregoir
authored and
namasikanam
committed
make casts from existing single sided formulas to two sided ones use a more robust pattern

oskgo
authored and
namasikanam
committed
Remove dead-code in theory cloning code.

strub
authored and
namasikanam
committed
Kill warnings + unify flags for ci/dev dune environments

strub
authored and
namasikanam
committed
also swap memory types when swapping memories

oskgo
authored and
namasikanam
committed
In matching, do not unify a memory with itself

strub
authored and
namasikanam
committed
Improve error message in to-assumption rewrite

strub
authored and
namasikanam
committed
When doing section-analysis, recurse in operators body

strub
authored and
namasikanam
committed
When doing section-analysis, recurse in types body

strub
authored and
namasikanam
committed
Fix dependency analysis

strub
authored and
namasikanam
committed
Build: unify release/dev warnings flags

strub
authored and
namasikanam
committed
fix dockerfiles

fdupress
authored and
namasikanam
committed
add a formosa dockerfile

fdupress
authored and
namasikanam
committed
[eco]: add a compilation trace (messages + goals)

strub
authored and
namasikanam
committed
fix the free memory of the second goal of `byehoare`
namasikanam
committed
feat: new source-documented lazy/eager logic.

loutr
authored and
namasikanam
committed
Refman skeleton.

strub
authored and
namasikanam
committed
CI (doc): not cancellable

strub
authored and
namasikanam
committed
style: use regular datatype for ty_body

loutr
authored and
namasikanam
committed
style: correct spelling of 'instantiate'

loutr
authored and
namasikanam
committed
feat: positivity check in type constructors with stack-based error reports

loutr
authored and
namasikanam
committed
fix alpha-conversion problems in ehoare

bgregoir
authored and
namasikanam
committed
another example for eHoare
namasikanam
committed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Another example for eHoare#845

Another example for eHoare#845
namasikanam wants to merge 26 commits intomainfrom
eHoare-example

Commits on Jan 30, 2026

Documentation comments and corresponding HTML generation.

fix handling of bounds in conseq equiv phoare

add manual trivial application to conseq variant (#848)

reduce when needed in proc and call rules (#849)

make casts from existing single sided formulas to two sided ones use a more robust pattern

Remove dead-code in theory cloning code.

Kill warnings + unify flags for ci/dev dune environments

also swap memory types when swapping memories

In matching, do not unify a memory with itself

Improve error message in to-assumption rewrite

When doing section-analysis, recurse in operators body

When doing section-analysis, recurse in types body

Fix dependency analysis

Build: unify release/dev warnings flags

fix dockerfiles

add a formosa dockerfile

[eco]: add a compilation trace (messages + goals)

fix the free memory of the second goal of `byehoare`

feat: new source-documented lazy/eager logic.

Refman skeleton.

CI (doc): not cancellable

style: use regular datatype for ty_body

style: correct spelling of 'instantiate'

feat: positivity check in type constructors with stack-based error reports

fix alpha-conversion problems in ehoare

another example for eHoare