🍬 Never.v

Proofs

Gitlab

Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.

Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Script_typed_ir.

Require TezosOfOCaml.Environment.V8.Proofs.Compare.

Definition compare (x y : Script_typed_ir.never) : int :=
  0.

Lemma compare_is_valid : Compare.Valid.t (fun _ ⇒ True) id compare.
Proof.
  easy.
Qed.