hax icon indicating copy to clipboard operation
hax copied to clipboard
verified publisher icon hacspec

Support default methods

Open W95Psp opened this issue 1 year ago • 4 comments

Following https://github.com/hacspec/hax/pull/824 and https://github.com/hacspec/hax/issues/624

Currently, neither Lean nor F* support default implementation in trait definitions.

W95Psp avatar Sep 16 '24 06:09 W95Psp

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] avatar Dec 12 '24 02:12 github-actions[bot]

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] avatar May 15 '25 00:05 github-actions[bot]

Related to https://github.com/cryspen/hax-evit/issues/24

W95Psp avatar Jun 16 '25 12:06 W95Psp

Having this checkable in F* is essential for checking embedded-cal – doing without provided methods would take away any API extensibility there.

chrysn avatar Nov 20 '25 16:11 chrysn