Skip to main content

🎫 Ticket_token.v

Translated OCaml

See proofs, Gitlab , OCaml

File generated by coq-of-ocaml
Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.

Require TezosOfOCaml.Proto_alpha.Alpha_context.
Require TezosOfOCaml.Proto_alpha.Script_typed_ir.
Require TezosOfOCaml.Proto_alpha.Ticket_scanner.

Records for the constructor parameters
Module ConstructorRecords_ex_token.
  Module ex_token.
    Module Ex_token.
      Record record {ticketer contents_type contents : Set} : Set := Build {
        ticketer : ticketer;
        contents_type : contents_type;
        contents : contents;
      }.
      Arguments record : clear implicits.
      Definition with_ticketer {t_ticketer t_contents_type t_contents} ticketer
        (r : record t_ticketer t_contents_type t_contents) :=
        Build t_ticketer t_contents_type t_contents ticketer r.(contents_type)
          r.(contents).
      Definition with_contents_type {t_ticketer t_contents_type t_contents}
        contents_type (r : record t_ticketer t_contents_type t_contents) :=
        Build t_ticketer t_contents_type t_contents r.(ticketer) contents_type
          r.(contents).
      Definition with_contents {t_ticketer t_contents_type t_contents} contents
        (r : record t_ticketer t_contents_type t_contents) :=
        Build t_ticketer t_contents_type t_contents r.(ticketer)
          r.(contents_type) contents.
    End Ex_token.
    Definition Ex_token_skeleton := Ex_token.record.
  End ex_token.
End ConstructorRecords_ex_token.
Import ConstructorRecords_ex_token.

Reserved Notation "'ex_token.Ex_token".

Inductive ex_token : Set :=
| Ex_token : {a : Set}, 'ex_token.Ex_token a ex_token

where "'ex_token.Ex_token" :=
  (fun (t_a : Set) ⇒ ex_token.Ex_token_skeleton Alpha_context.Contract.t
    Script_typed_ir.comparable_ty t_a).

Module ex_token.
  Include ConstructorRecords_ex_token.ex_token.
  Definition Ex_token := 'ex_token.Ex_token.
End ex_token.

Definition token_and_amount_of_ex_ticket
  (function_parameter : Ticket_scanner.ex_ticket)
  : ex_token × Alpha_context.Script_int.num :=
  let
    'Ticket_scanner.Ex_ticket contents_type {|
      Script_typed_ir.ticket.ticketer := ticketer;
        Script_typed_ir.ticket.contents := contents;
        Script_typed_ir.ticket.amount := amount
        |} := function_parameter in
  ((Ex_token
    {| ex_token.Ex_token.ticketer := ticketer;
      ex_token.Ex_token.contents_type := contents_type;
      ex_token.Ex_token.contents := contents; |}), amount).