Code

Allow ensures and requires on traits#790

Code

Merged

W95Psp merged 11 commits intomainhacspec/hax:mainfrom pre-post-traitshacspec/hax:pre-post-traitsCopy head branch name to clipboardJul 22, 2024

+575-204

Commits

Commits on Jul 22, 2024

• cleanup(backends/f*): remove deadcode

  W95Psp

  committed
  9542f4c

  Copy full SHA for 9542f4c

• feat(engine/print_rust): print attrs on impl and traits

  W95Psp

  committed
  5dba29c

  Copy full SHA for 5dba29c

• chore(engine): kill dead code

  W95Psp

  committed
  6e71931

  Copy full SHA for 6e71931

• feat(backends/fstar/ast): add implies

  W95Psp

  committed
  cfd271c

  Copy full SHA for cfd271c

• feat(backends/fstar): add FStarBinder.of_named_typ

  W95Psp

  committed
  ed03d7a

  Copy full SHA for ed03d7a

• feat(engine/ast-utils): add make_lets

  W95Psp

  committed
  663e966

  Copy full SHA for 663e966

• feat(hax-lib-macros): improve expect_ident utils

  W95Psp

  committed
  16ce68e

  Copy full SHA for 16ce68e

• feat: allow pre/post on traits (fixes #731)

  W95Psp

  committed
  93cc58d

  Copy full SHA for 93cc58d

• chore: dune fmt

  W95Psp

  committed
  61409d1

  Copy full SHA for 61409d1

• chore: remove debug code

  W95Psp

  committed
  91c8763

  Copy full SHA for 91c8763

• chore: udpate test snapshots

  W95Psp

  committed
  d2ebf7e

  Copy full SHA for d2ebf7e