Missing rewrite for `Constant.op` (?)
landonf opened this issue · 0 comments
landonf commented
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.