🎫 Ticket_token.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_token.

Require TezosOfOCaml.Proto_alpha.Proofs.Ticket_scanner.

Lemma token_and_amount_of_ex_ticket_is_valid ex_ticket :
  Ticket_scanner.Ex_ticket.Valid.t ex_ticket →
  let '(_, Alpha_context.Script_int.Num_tag amount) :=
      Ticket_token.token_and_amount_of_ex_ticket ex_ticket in
  0 ≤ amount.
  intros [? ? [? ? []] H]; apply H.
Qed.