Support for monomorphization over regular values like trait methods

FStarLang / karamel

KaRaMeL is a tool for extracting low-level F* programs to readable C code

Apache License 2.0

394 stars 58 forks source link

Support for monomorphization over regular values like trait methods #431

Closed msprotz closed 3 months ago

msprotz commented 3 months ago

This is in support of https://github.com/AeneasVerif/eurydice/pull/11 which needs to build against this.

Both PRs will be merged at the same time; basically, this adds the option to monomorphize over an additional set of values that do not pertain to const generics and therefore are not bound in types (like const generics).

msprotz commented 3 months ago

Got a local Everest green (after disabling miTLS extraction, per discussion)