🍃 RPC_arg.v
Environment
Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.
Require TezosOfOCaml.Environment.Structs.V0.Pervasives.
Module t.
Record record {a : Set} : Set := Build {
descr : option string;
name : string;
destruct : string → Pervasives.result a string;
construct : a → string;
}.
Arguments record : clear implicits.
End t.
Definition t := t.record.
Definition arg (a : Set) : Set := t a.
Definition make {a : Set}
(descr : option string) (name : string)
(destruct : string → Pervasives.result a string) (construct : a → string)
(_ : unit) : arg a :=
t.Build _ descr name destruct construct.
Module descr.
Record record : Set := Build {
name : string;
descr : option string }.
Definition with_name name (r : record) :=
Build name r.(descr).
Definition with_descr descr (r : record) :=
Build r.(name) descr.
End descr.
Definition descr := descr.record.
Definition descr_value {a : Set} (x : arg a) : descr :=
{|
descr.name := x.(t.name);
descr.descr := x.(t.descr);
|}.
Parameter bool_value : arg bool.
Parameter int_value : arg int.
Parameter uint : arg int.
Parameter int32_value : arg int32.
Parameter uint31 : arg int32.
Parameter int64_value : arg int64.
Parameter uint63 : arg int64.
Parameter string_value : arg string.
Parameter option_value : ∀ {a : Set}, arg a → arg (option a).
Parameter list_value : ∀ {a : Set}, arg a → arg (list a).
Parameter like : ∀ {a : Set}, arg a → option string → string → arg a.
Inductive eq (a : Set) : Set :=
| Eq : eq a.
Arguments Eq {_}.
Parameter eq_value : ∀ {a b : Set}, arg a → arg b → option (eq a).
Require Import CoqOfOCaml.Settings.
Require TezosOfOCaml.Environment.Structs.V0.Pervasives.
Module t.
Record record {a : Set} : Set := Build {
descr : option string;
name : string;
destruct : string → Pervasives.result a string;
construct : a → string;
}.
Arguments record : clear implicits.
End t.
Definition t := t.record.
Definition arg (a : Set) : Set := t a.
Definition make {a : Set}
(descr : option string) (name : string)
(destruct : string → Pervasives.result a string) (construct : a → string)
(_ : unit) : arg a :=
t.Build _ descr name destruct construct.
Module descr.
Record record : Set := Build {
name : string;
descr : option string }.
Definition with_name name (r : record) :=
Build name r.(descr).
Definition with_descr descr (r : record) :=
Build r.(name) descr.
End descr.
Definition descr := descr.record.
Definition descr_value {a : Set} (x : arg a) : descr :=
{|
descr.name := x.(t.name);
descr.descr := x.(t.descr);
|}.
Parameter bool_value : arg bool.
Parameter int_value : arg int.
Parameter uint : arg int.
Parameter int32_value : arg int32.
Parameter uint31 : arg int32.
Parameter int64_value : arg int64.
Parameter uint63 : arg int64.
Parameter string_value : arg string.
Parameter option_value : ∀ {a : Set}, arg a → arg (option a).
Parameter list_value : ∀ {a : Set}, arg a → arg (list a).
Parameter like : ∀ {a : Set}, arg a → option string → string → arg a.
Inductive eq (a : Set) : Set :=
| Eq : eq a.
Arguments Eq {_}.
Parameter eq_value : ∀ {a b : Set}, arg a → arg b → option (eq a).