🍬 Never.v
Proofs
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.
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.