Code

Add support for math integers#629

Code

Merged

W95Psp merged 24 commits intomaincryspen/hax:mainfrom math-integerscryspen/hax:math-integersCopy head branch name to clipboardApr 30, 2024

+685-1

Commits

Commits on Apr 30, 2024

• feat(engine/utils): add apply

  W95Psp

  committed
  d62dd81

  Copy full SHA for d62dd81

• feat(hax-lib): add Makefile

  W95Psp

  committed
  5e0ddf5

  Copy full SHA for 5e0ddf5

• feat(hax-lib): add a Int type that models math. integers

  W95Psp

  committed
  8e188d8

  Copy full SHA for 8e188d8

• feat(engine): intro. names for mathematical integers

  W95Psp

  committed
  9f397a2

  Copy full SHA for 9f397a2

• feat(engine): intro new phase specialize

  W95Psp

  committed
  7f502ff

  Copy full SHA for 7f502ff

• feat(F*): interpret _unsafe_from_str as literals

  W95Psp

  committed
  2ff5b82

  Copy full SHA for 2ff5b82

• feat(fstar): resugar math int functions into operators

  W95Psp

  committed
  b47afc0

  Copy full SHA for b47afc0

• feat(fstar): use phase specialize

  W95Psp

  committed
  8441791

  Copy full SHA for 8441791

• feat(macros): add a int! macro

  W95Psp

  committed
  61ccd43

  Copy full SHA for 61ccd43

• tests: math integers

  W95Psp

  committed
  fb2ee4a

  Copy full SHA for fb2ee4a

• chore: refresh tests

  W95Psp

  committed
  9489faf

  Copy full SHA for 9489faf

• fix(hax-lib): num-* deps: disable default features

  W95Psp

  committed
  ea997c6

  Copy full SHA for ea997c6

• fix: tweak versions for hacspec lib issues...

  W95Psp

  committed
  4f5a0b9

  Copy full SHA for 4f5a0b9

• fix(hax-lib): int: bump BYTES to 1024

  W95Psp

  committed
  39109fd

  Copy full SHA for 39109fd

• doc(hax-lib): bigint: add doc & change visibility

  W95Psp

  committed
  0c8c310

  Copy full SHA for 0c8c310

• fix(hax-lib): missing newline

  W95Psp

  committed
  c715876

  Copy full SHA for c715876

• fix(hax-lib): int: specify which kind of digit

  W95Psp

  committed
  714db89

  Copy full SHA for 714db89

• fix(hax-lib): Cargo.toml: remove redundant features field

  W95Psp

  committed
  16aa152

  Copy full SHA for 16aa152

• fix(hax-lib): Cargo.toml: use hax-lib-macros from workspace

  W95Psp

  committed
  e24ae94

  Copy full SHA for e24ae94

• fix(hax-lib): int: no need for exclude flags

  Show description for 7b46dac
  W95Psp

  committed
  7b46dac

  Copy full SHA for 7b46dac

• feat(hax-lib): restore/add feature macros

  W95Psp

  committed
  a917e40

  Copy full SHA for a917e40

• fix: name

  W95Psp

  committed
  62dd5d3

  Copy full SHA for 62dd5d3

• fix(hax-lib): int: expose int! if feature="macros"

  W95Psp

  committed
  232cc5d

  Copy full SHA for 232cc5d

• refactor(engine): specialize phase: cleanup & comments

  W95Psp

  committed
  fc6b832

  Copy full SHA for fc6b832