🎫 Ticket_scanner.v

Proofs

See code, Gitlab , OCaml

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

Require Import TezosOfOCaml.Proto_alpha.Environment.
Require TezosOfOCaml.Proto_alpha.Ticket_scanner.

Require TezosOfOCaml.Proto_alpha.Proofs.Script_typed_ir.

Module Ex_ticket.
  Module Valid.
    Inductive t : Ticket_scanner.ex_ticket → Prop :=
    | Intro {a} :
      ∀ ty ticket,
      Script_typed_ir.Ticket.Valid.t ticket →
      t (Ticket_scanner.Ex_ticket (a := a) ty ticket).
  End Valid.
End Ex_ticket.