FStarLang/karamel

Kremlin attempts to extract projectors of inductives marked as noextract

Closed this issue · 0 comments

module M
noextract type t = { x:bool }
$ krml M.fst
...
✔ [F*] ⏱️ <1ms
Cannot re-check M.__proj__C__item__x as valid Low* and will not extract it.  If M.__proj__C__item__x is not meant to be extracted, consider marking it as Ghost, noextract, or using a bundle. If it is meant to be extracted, use -dast for further debugging.

Warning 4: in top-level declaration M.__proj__C__item__x, in file M: Malformed input:
Reference to undefined type: M.t

Same for noextract type t = | C: x:bool -> t