Kremlin attempts to extract projectors of inductives marked as noextract
Closed this issue · 0 comments
s-zanella commented
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