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.

贡献者指南