Make only `visitors` opaque, not `show`

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

Closed W95Psp closed 3 months ago

W95Psp commented 3 months ago

Without namespacing, both the visitor PPX and the show PPX read the opaque attribute: this PR adds a visitor in front of a few opaque attributes.

Seems like K.poly_comp itself has no show derivation, whence the show.opaque.

msprotz commented 3 months ago

Great thanks!