Code

Erase functions to fun#3661

Code

Open

gebner wants to merge 5 commits intomasterFStarLang/FStar:masterfrom gebner_erase_funFStarLang/FStar:gebner_erase_funCopy head branch name to clipboard

+210-179

Commits

Commits on Jan 16, 2025

• Replace must_erase_during_extraction with erasable.

  gebner

  committed
  49d1f2e

  Copy full SHA for 49d1f2e

• Erase functions to functions instead of unit.

  Show description for 9218344
  gebner

  committed
  9218344

  Copy full SHA for 9218344

• Correctly erased n-ary ghost functions.

  gebner

  committed
  d79ac67

  Copy full SHA for d79ac67

• Suppress erasable warning for props.

  gebner

  committed
  8f4c410

  Copy full SHA for 8f4c410

• Fix test.

  gebner

  committed
  9a3867d

  Copy full SHA for 9a3867d