Mentions légales du service

Skip to content

[extraction] Declare equality operator transparent.

It seems this should be defined, and have Coq not to have to handle this Qed specially; code is nicely generated by extraction:

  let eqb_dec k k1 k2 =
    let b = k.Keys_Base.eqb k1 k2 in if b then Left else Right

Merge request reports