FStarLang/karamel

Missing rewrite for `Constant.op` (?)

landonf opened this issue · 0 comments

Test case:

module OpEq

let compare' (#a:eqtype)
  (eq:(a -> a -> Tot bool) { eq == op_Equality #a })
  (a1 a2:a)
: bool
= a1 `eq` a1

inline_for_extraction noextract
let compare (#a:eqtype) (a1 a2: a): bool
= compare' (op_Equality #a) a1 a2

let example (x y: UInt32.t) = x `compare` y

Produces:

> krml OpEq.fst   
...
✔ [AstToCStar] ⏱️ <1ms
Fatal exception raised in OpEq_example
Fatal error: exception Failure("[mk_expr m]: op should've been caught")

I'm required to state: Not a Contribution.