FStarLang/FStar

assert are never extracted even with `--mlish`

Open

#984 建立於 2017年4月13日

在 GitHub 查看
 (0 留言) (0 反應) (0 負責人)F* (258 fork)auto 404
area/error-messagescomponent/extractiongood first issue

倉庫指標

Star
 (3,068 star)
PR 合併指標
 (PR 指標待抓取)

描述

The function assert is never extracted to OCaml. This is not very nice when using the ocaml-based F* compiler and getting a Failure("Impossible") because an invariant was broken.

It would be nice to extract the assertions when they do correspond to runtime checks as they are in the compiler.

貢獻者指南