Code

Opaque extensions#1134

Code

Merged

maximebuyse merged 17 commits intomainhacspec/hax:mainfrom opaque-extensionshacspec/hax:opaque-extensionsCopy head branch name to clipboardDec 12, 2024

+511-150

Commits

Commits on Dec 5, 2024

• Unify (an extended version of) opaque and interface-only in a single erasure mechanism.

  maximebuyse

  committed
  e2aa8b8

• Add tests for opaque attribute.

  maximebuyse

  committed
  1af618e

• Tests snapshots.

  maximebuyse

  committed
  f3fb4d5

• Update documentation of -i flag.

  maximebuyse

  committed
  3282b7e

• Allow to make opaque (and drop body) of selected (non-trait) impl methods.

  maximebuyse

  committed
  ef18a4f

• Document and correct.

  maximebuyse

  committed
  5574e81

• Allow opaque types even without interface mode.

  maximebuyse

  committed
  ed3ef5c

• Add function signature only in interface mode.

  maximebuyse

  committed
  30ec986

• New tests snapshots.

  maximebuyse

  committed
  cdcd4fb

• Remove body of methods inside impls in type-only mode.

  maximebuyse

  committed
  f300ff8

• Pass generic arguments to erased impls.

  maximebuyse

  committed
  a9f56d8

• Remove the implementation without FStarBinder of erased_impl.

  maximebuyse

  committed
  cc2a7f9

• Rename NeverDropBody to NeverErased.

  maximebuyse

  committed
  b9f31e4

• Updated tests.

  maximebuyse

  committed
  c5dc718

Commits on Dec 12, 2024

• Merge branch 'main' into opaque-extensions

  W95Psp

  authored
  769f700

• Add more cases in opaque tests.

  maximebuyse

  committed
  b3de817

• Go back to previous behaviour for val interfaces in the fsti for impls with assoc type.

  maximebuyse

  committed
  7629b15