FStarLang/FStar

assert are never extracted even with `--mlish`

Open

#984 opened on 2017年4月13日

GitHub で見る
 (0 comments) (0 reactions) (0 assignees)F* (258 forks)auto 404
area/error-messagescomponent/extractiongood first issue

Repository metrics

Stars
 (3,068 stars)
PR merge metrics
 (PR metrics pending)

説明

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.

コントリビューターガイド