search

hacspec / hax

A Rust verification tool
https://hacspec.org/blog
Apache License 2.0
198 stars 21 forks source link

Engine: F*: option to extract opaque interfaces for impls #768

Open W95Psp opened 4 months ago

W95Psp commented 4 months ago

Currently, we export interfaces for impls with full-blown associated functions, constants and types definitions in the fstis files. This is a big issue when we want to extract a signature: this behavior yields the extraction of loads of other depending items.

Probably related to #616

github-actions[bot] commented 2 months ago

This issue has been marked as stale due to a lack of activity for 60 days. If you believe this issue is still relevant, please provide an update or comment to keep it open. Otherwise, it will be closed in 7 days.

github-actions[bot] commented 2 months ago

This issue has been closed due to a lack of activity since being marked as stale. If you believe this issue is still relevant, please reopen it with an update or comment.

W95Psp commented 1 month ago

This is something we need and want