package archetype

  1. Overview
  2. Docs
package archetype
Legend:
Library
Module
Module type
Parameter
Class
Class type
val show_lident : lident -> Ppx_deriving_runtime.string
type namespace = lident
val show_namespace : namespace -> Ppx_deriving_runtime.string
type longident = namespace option * lident
val show_longident : longident -> Ppx_deriving_runtime.string
val unloc_longident : longident -> Ident.ident option * Ident.ident
val pp_ident : Format.formatter -> string -> unit
val pp_lident : Format.formatter -> string Location.loced -> unit
type container =
  1. | Collection
  2. | Aggregate
  3. | Partition
  4. | AssetContainer
  5. | AssetKey
  6. | AssetValue
  7. | AssetView
val show_container : container -> Ppx_deriving_runtime.string
type currency =
  1. | Utz
val show_currency : currency -> Ppx_deriving_runtime.string
type vtyp =
  1. | VTunit
  2. | VTbool
  3. | VTnat
  4. | VTint
  5. | VTrational
  6. | VTdate
  7. | VTduration
  8. | VTstring
  9. | VTaddress
  10. | VTcurrency
  11. | VTkey
  12. | VTkeyhash
  13. | VTsignature
  14. | VTbytes
  15. | VTchainid
  16. | VTbls12_381_fr
  17. | VTbls12_381_g1
  18. | VTbls12_381_g2
  19. | VTnever
  20. | VTchest
  21. | VTchest_key
  22. | VTtx_rollup_l2_address
type trtyp =
  1. | TRentry
  2. | TRaction
  3. | TRasset
  4. | TRfield
type ptyp =
  1. | Tnamed of int
  2. | Tasset of longident
  3. | Trecord of longident
  4. | Tevent of longident
  5. | Tenum of longident
  6. | Tbuiltin of vtyp
  7. | Tcontainer of type_ * container
  8. | Tset of type_
  9. | Tlist of type_
  10. | Tmap of type_ * type_
  11. | Tbig_map of type_ * type_
  12. | Titerable_big_map of type_ * type_
  13. | Tor of type_ * type_
  14. | Tlambda of type_ * type_
  15. | Ttuple of type_ list
  16. | Toption of type_
  17. | Toperation
  18. | Tcontract of type_
  19. | Ttrace of trtyp
  20. | Tticket of type_
  21. | Tsapling_state of int
  22. | Tsapling_transaction of int
and type_ = ptyp
val pp_type_ : Ppx_deriving_runtime.Format.formatter -> type_ -> Ppx_deriving_runtime.unit
val show_type_ : type_ -> Ppx_deriving_runtime.string
type logical_operator =
  1. | And
  2. | Or
  3. | Xor
  4. | Imply
  5. | Equiv
val show_logical_operator : logical_operator -> Ppx_deriving_runtime.string
type comparison_operator =
  1. | Equal
  2. | Nequal
  3. | Gt
  4. | Ge
  5. | Lt
  6. | Le
val show_comparison_operator : comparison_operator -> Ppx_deriving_runtime.string
type assignment_operator =
  1. | ValueAssign
  2. | PlusAssign
  3. | MinusAssign
  4. | MultAssign
  5. | DivAssign
  6. | AndAssign
  7. | OrAssign
val show_assignment_operator : assignment_operator -> Ppx_deriving_runtime.string
type arithmetic_operator =
  1. | Plus
  2. | Minus
  3. | Mult
  4. | DivRat
  5. | DivEuc
  6. | Modulo
  7. | DivMod
  8. | ThreeWayCmp
  9. | ShiftLeft
  10. | ShiftRight
val show_arithmetic_operator : arithmetic_operator -> Ppx_deriving_runtime.string
type unary_arithmetic_operator =
  1. | Uminus
val show_unary_arithmetic_operator : unary_arithmetic_operator -> Ppx_deriving_runtime.string
type operator = [
  1. | `Logical of logical_operator
  2. | `Cmp of comparison_operator
  3. | `Arith of arithmetic_operator
  4. | `Unary of unary_arithmetic_operator
  5. | `Assign of assignment_operator
]
val show_operator : operator -> Ppx_deriving_runtime.string
type const =
  1. | Cstate
  2. | Cnow
  3. | Ctransferred
  4. | Ccaller
  5. | Cfail
  6. | Cbalance
  7. | Csource
  8. | Cselfaddress
  9. | Cconditions
  10. | Centries
  11. | Cnone
  12. | Cany
  13. | Canyentry
  14. | Cresult
  15. | Cselfchainid
  16. | Coperations
  17. | Cmetadata
  18. | Clevel
  19. | Cadd
  20. | Cput
  21. | Caddupdate
  22. | Cceil
  23. | Cclear
  24. | Cconcat
  25. | Ccontains
  26. | Ccount
  27. | Cfloor
  28. | Cget
  29. | Cgetopt
  30. | Cisnone
  31. | Cissome
  32. | Cinttonat
  33. | Clength
  34. | Cmax
  35. | Cmin
  36. | Cnth
  37. | Cpack
  38. | Cremove
  39. | Cremoveall
  40. | Cremoveif
  41. | Cselect
  42. | Cslice
  43. | Csort
  44. | Csum
  45. | Cunpack
  46. | Cupdate
  47. | Cupdateall
  48. | Cmakeoperation
  49. | Cmakeevent
  50. | Cnattostring
  51. | Cbytestonat
  52. | Cnattobytes
  53. | Cbytestoint
  54. | Cinttobytes
  55. | Cexec
  56. | Capply
  57. | Cinttodate
  58. | CmutezToNat
  59. | Csetdelegate
  60. | Ckeyhashtocontract
  61. | Csubnat
  62. | Csubmutez
  63. | Cgreedyand
  64. | Cgreedyor
  65. | CmakeAsset
  66. | CtoContainer
  67. | CputRemove
  68. | CgetEntrypoint
  69. | CrequireEntrypoint
  70. | CcallView
  71. | CimportCallView
  72. | Csimplifyrational
  73. | Cgetnumerator
  74. | Cgetdenominator
  75. | Csadd
  76. | Csremove
  77. | Csupdate
  78. | Cscontains
  79. | Cslength
  80. | Chead
  81. | Ctail
  82. | Cabs
  83. | Cprepend
  84. | Creverse
  85. | Cmput
  86. | Cmremove
  87. | Cmupdate
  88. | Cmget
  89. | Cmgetopt
  90. | Cmcontains
  91. | Cmlength
  92. | Cblake2b
  93. | Csha256
  94. | Csha512
  95. | Csha3
  96. | Ckeccak
  97. | Cchecksignature
  98. | Ckeytokeyhash
  99. | Ccontracttoaddress
  100. | Caddresstocontract
  101. | Ckeytoaddress
  102. | Ctotalvotingpower
  103. | Cvotingpower
  104. | Cminblocktime
  105. | Ccreateticket
  106. | Creadticket
  107. | Csplitticket
  108. | Cjointickets
  109. | Csapling_empty_state
  110. | Csapling_verify_update
  111. | Cpairing_check
  112. | Copen_chest
  113. | Cemit
  114. | Cbefore
  115. | Citerated
  116. | Ctoiterate
  117. | Cempty
  118. | Cisempty
  119. | Csingleton
  120. | Csubsetof
  121. | Cunion
  122. | Cinter
  123. | Cdiff
type 'node struct_poly = {
  1. node : 'node;
  2. type_ : type_ option;
  3. label : Ident.ident option;
  4. loc : Location.t;
}
type qualid = qualid_node struct_poly
and qualid_node =
  1. | Qident of lident
  2. | Qdot of qualid * lident
val show_qualid : qualid -> Ppx_deriving_runtime.string
val show_qualid_node : qualid_node -> Ppx_deriving_runtime.string
type sexpr = sexpr_node struct_poly
and sexpr_node =
  1. | Sref of lident
  2. | Sor of sexpr * sexpr
  3. | Sany
val show_sexpr_node : sexpr_node -> Ppx_deriving_runtime.string
and bval_node =
  1. | BVint of Core.big_int
  2. | BVnat of Core.big_int
  3. | BVbool of bool
  4. | BVrational of Core.big_int * Core.big_int
  5. | BVdate of Core.date
  6. | BVstring of string
  7. | BVcurrency of currency * Core.big_int
  8. | BVaddress of string
  9. | BVtx_rollup_l2_address of string
  10. | BVduration of Core.duration
  11. | BVbytes of string
  12. | BVunit
val show_bval_node : bval_node -> Ppx_deriving_runtime.string
type quantifier =
  1. | Forall
  2. | Exists
val show_quantifier : quantifier -> Ppx_deriving_runtime.string
type pattern = pattern_node struct_poly
and pattern_node =
  1. | Mwild
  2. | Mconst of lident * lident list
val show_pattern : pattern -> Ppx_deriving_runtime.string
val show_pattern_node : pattern_node -> Ppx_deriving_runtime.string
type call_kind =
  1. | Cid of lident
  2. | Cconst of const
val show_call_kind : call_kind -> Ppx_deriving_runtime.string
type var_temporality =
  1. | VTbefore
  2. | VTat of Ident.ident
  3. | VTnone
val show_var_temporality : var_temporality -> Ppx_deriving_runtime.string
type vset =
  1. | Vadded
  2. | Vremoved
  3. | Vunmoved
  4. | Vnone
type michelson_struct = {
  1. ms_content : Michelson.obj_micheline;
}
val show_michelson_struct : michelson_struct -> Ppx_deriving_runtime.string
type pterm = pterm_node struct_poly
and pterm_node =
  1. | Pquantifer of quantifier * lident * pterm option * type_ * pterm
  2. | Pif of pterm * pterm * pterm
  3. | Pmatchwith of pterm * (pattern * pterm) list
  4. | Pmatchoption of pterm * lident * pterm * pterm
  5. | Pmatchor of pterm * lident * pterm * lident * pterm
  6. | Pmatchlist of pterm * lident * lident * pterm * pterm
  7. | Pfold of pterm * lident * pterm
  8. | Pmap of pterm * lident * pterm
  9. | Pcall of pterm option * call_kind * type_ list * pterm_arg list
  10. | Plogical of logical_operator * pterm * pterm
  11. | Pnot of pterm
  12. | Pmulticomp of pterm * (comparison_operator * pterm) list
  13. | Pcomp of comparison_operator * pterm * pterm
  14. | Parith of arithmetic_operator * pterm * pterm
  15. | Puarith of unary_arithmetic_operator * pterm
  16. | Precord of pterm list
  17. | Precupdate of pterm * (lident * pterm) list
  18. | Pletin of lident * pterm * type_ option * pterm * pterm option
  19. | Pdeclvar of lident * type_ option * pterm * bool
  20. | Pvar of var_temporality * vset * longident
  21. | Parray of pterm list
  22. | Plit of bval
  23. | Pdot of pterm * lident
  24. | Pquestiondot of pterm * lident
  25. | Pconst of const
  26. | Ptuple of pterm list
  27. | Ptupleaccess of pterm * Core.big_int
  28. | Pnone
  29. | Psome of pterm
  30. | Pleft of type_ * pterm
  31. | Pright of type_ * pterm
  32. | Plambda of type_ * lident * type_ * pterm
  33. | Pcast of type_ * type_ * pterm
  34. | Pself of lident
  35. | Pternary of pterm * pterm * pterm
  36. | Pcreatecontract of michelson_struct * pterm * pterm * pterm
and pterm_arg =
  1. | AExpr of pterm
  2. | AFun of lident * type_ * (lident * type_ * pterm) list * pterm
  3. | AEffect of (lident * operator * pterm) list
  4. | ASorting of bool * lident
  5. | AIdent of lident
val show_pterm_node : pterm_node -> Ppx_deriving_runtime.string
val show_pterm_arg : pterm_arg -> Ppx_deriving_runtime.string
type instruction = {
  1. node : instruction_node;
  2. label : string option;
  3. loc : Location.t;
}
and transfer_t =
  1. | TTsimple of pterm * pterm
  2. | TTcontract of pterm * pterm * lident * type_ * pterm
  3. | TTentry of pterm * pterm * pterm
  4. | TTgen of pterm * Ident.ident * Ident.ident * type_ * pterm * pterm
  5. | TTself of pterm * lident * (lident * pterm) list
  6. | TToperation of pterm
and detach_kind =
  1. | DK_option of type_ * Ident.ident
  2. | DK_map of type_ * Ident.ident * pterm
and instruction_node =
  1. | Iif of pterm * instruction * instruction
  2. | Ifor of for_ident * pterm * instruction
  3. | Iiter of lident * pterm * pterm * instruction
  4. | Iwhile of pterm * instruction
  5. | Iletin of lident * pterm * instruction
  6. | Ideclvar of lident * pterm * bool
  7. | Ideclvaropt of lident * pterm * pterm option * bool
  8. | Iseq of instruction list
  9. | Imatchwith of pterm * (pattern * instruction) list
  10. | Imatchoption of pterm * lident * instruction * instruction
  11. | Imatchor of pterm * lident * instruction * lident * instruction
  12. | Imatchlist of pterm * lident * lident * instruction * instruction
  13. | Iassign of assignment_operator * type_ * lvalue * pterm * pterm option
  14. | Irequire of bool * pterm * pterm
  15. | Itransfer of transfer_t
  16. | Iemit of lident * pterm
  17. | Icall of pterm option * call_kind * pterm_arg list
  18. | Ireturn of pterm
  19. | Ilabel of lident
  20. | Ifail of pterm
  21. | Ifailsome of pterm
  22. | Idetach of lident * detach_kind * type_ * pterm
and for_ident =
  1. | FIsimple of lident
  2. | FIdouble of lident * lident
and lvalue = [
  1. | `Var of lident
  2. | `Field of longident * pterm * lident
  3. | `Asset of longident * pterm * lident
  4. | `Tuple of pterm * int * int
]
val show_instruction : instruction -> Ppx_deriving_runtime.string
val show_transfer_t : transfer_t -> Ppx_deriving_runtime.string
val show_detach_kind : detach_kind -> Ppx_deriving_runtime.string
val show_instruction_node : instruction_node -> Ppx_deriving_runtime.string
val show_for_ident : for_ident -> Ppx_deriving_runtime.string
val show_lvalue : lvalue -> Ppx_deriving_runtime.string
type decl_gen = {
  1. name : lident;
  2. typ : type_ option;
  3. default : pterm option;
  4. shadow : bool;
  5. loc : Location.t;
}
val show_decl_gen : decl_gen -> Ppx_deriving_runtime.string
type label_term = {
  1. label : lident option;
  2. term : pterm;
  3. error : pterm option;
  4. loc : Location.t;
}
val show_label_term : label_term -> Ppx_deriving_runtime.string
type variable_kind =
  1. | VKconstant
  2. | VKvariable
val show_variable_kind : variable_kind -> Ppx_deriving_runtime.string
type variable = {
  1. decl : decl_gen;
  2. kind : variable_kind;
  3. invs : label_term list;
  4. loc : Location.t;
}
val show_variable : variable -> Ppx_deriving_runtime.string
type predicate = {
  1. name : lident;
  2. args : (lident * type_) list;
  3. body : pterm;
  4. loc : Location.t;
}
val show_predicate : predicate -> Ppx_deriving_runtime.string
type definition = {
  1. name : lident;
  2. typ : type_;
  3. var : lident;
  4. body : pterm;
  5. loc : Location.t;
}
val show_definition : definition -> Ppx_deriving_runtime.string
type fail = {
  1. label : lident;
  2. fid : lident option;
  3. arg : lident;
  4. atype : type_;
  5. formula : pterm;
  6. loc : Location.t;
}
type invariant = {
  1. label : lident;
  2. formulas : pterm list;
}
val show_invariant : invariant -> Ppx_deriving_runtime.string
type postcondition = {
  1. name : lident;
  2. formula : pterm;
  3. invariants : invariant list;
  4. uses : lident list;
}
val show_postcondition : postcondition -> Ppx_deriving_runtime.string
type assert_ = {
  1. name : lident;
  2. label : lident;
  3. formula : pterm;
  4. invariants : invariant list;
  5. uses : lident list;
}
val pp_assert_ : Ppx_deriving_runtime.Format.formatter -> assert_ -> Ppx_deriving_runtime.unit
val show_assert_ : assert_ -> Ppx_deriving_runtime.string
type parameter = {
  1. name : lident;
  2. typ : type_;
  3. default : pterm option;
  4. value : pterm option;
  5. const : bool;
  6. loc : Location.t;
}
val show_parameter : parameter -> Ppx_deriving_runtime.string
type specification = {
  1. predicates : predicate list;
  2. definitions : definition list;
  3. fails : fail list;
  4. lemmas : label_term list;
  5. theorems : label_term list;
  6. variables : variable list;
  7. invariants : (lident * label_term list) list;
  8. effect : instruction option;
  9. specs : postcondition list;
  10. asserts : assert_ list;
  11. loc : Location.t;
}
val show_specification : specification -> Ppx_deriving_runtime.string
type entry_description =
  1. | ADAny
  2. | ADOp of string * lident
val pp_entry_description : Ppx_deriving_runtime.Format.formatter -> entry_description -> Ppx_deriving_runtime.unit
val show_entry_description : entry_description -> Ppx_deriving_runtime.string
type security_role = lident
val show_security_role : security_role -> Ppx_deriving_runtime.string
type security_entry =
  1. | Sany
  2. | Sentry of lident list
val pp_security_entry : Ppx_deriving_runtime.Format.formatter -> security_entry -> Ppx_deriving_runtime.unit
val show_security_entry : security_entry -> Ppx_deriving_runtime.string
type security_node =
  1. | SonlyByRole of entry_description * security_role list
  2. | SonlyInEntry of entry_description * security_entry
  3. | SonlyByRoleInEntry of entry_description * security_role list * security_entry
  4. | SnotByRole of entry_description * security_role list
  5. | SnotInEntry of entry_description * security_entry
  6. | SnotByRoleInEntry of entry_description * security_role list * security_entry
  7. | StransferredBy of entry_description
  8. | StransferredTo of entry_description
  9. | SnoStorageFail of security_entry
val show_security_node : security_node -> Ppx_deriving_runtime.string
type security_predicate = {
  1. s_node : security_node;
  2. loc : Location.t;
}
val show_security_predicate : security_predicate -> Ppx_deriving_runtime.string
type security_item = {
  1. label : lident;
  2. predicate : security_predicate;
  3. loc : Location.t;
}
val show_security_item : security_item -> Ppx_deriving_runtime.string
type security = {
  1. items : security_item list;
  2. loc : Location.t;
}
val show_security : security -> Ppx_deriving_runtime.string
type view_visibility =
  1. | VVonchain
  2. | VVonoffchain
  3. | VVoffchain
val show_view_visibility : view_visibility -> Ppx_deriving_runtime.string
type fun_kind =
  1. | FKfunction
  2. | FKgetter
  3. | FKview of view_visibility
val show_fun_kind : fun_kind -> Ppx_deriving_runtime.string
type function_ = {
  1. name : lident;
  2. kind : fun_kind;
  3. args : decl_gen list;
  4. body : instruction;
  5. specification : specification option;
  6. return : type_;
  7. loc : Location.t;
}
val pp_function_ : Ppx_deriving_runtime.Format.formatter -> function_ -> Ppx_deriving_runtime.unit
val show_function_ : function_ -> Ppx_deriving_runtime.string
type rexpr = rexpr_node struct_poly
and rexpr_node =
  1. | Rany
  2. | Rasset of longident
  3. | Rexpr of pterm
  4. | Ror of rexpr * rexpr
val show_rexpr_node : rexpr_node -> Ppx_deriving_runtime.string
type transition = {
  1. from : sexpr;
  2. on : (lident * type_ * lident * type_) option;
  3. trs : (lident * pterm option * instruction option) list;
}
val show_transition : transition -> Ppx_deriving_runtime.string
type transaction = {
  1. name : lident;
  2. args : decl_gen list;
  3. sourcedby : (rexpr * pterm option) option;
  4. calledby : (rexpr * pterm option) option;
  5. state_is : (lident * pterm option) option;
  6. accept_transfer : bool * pterm option;
  7. constants : label_term list option;
  8. require : label_term list option;
  9. failif : label_term list option;
  10. transition : transition option;
  11. specification : specification option;
  12. functions : function_ list;
  13. effect : instruction option;
  14. loc : Location.t;
}
val show_transaction : transaction -> Ppx_deriving_runtime.string
type enum_item_struct = {
  1. name : lident;
  2. initial : bool;
  3. invariants : label_term list;
  4. args : ptyp list;
  5. loc : Location.t;
}
val show_enum_item_struct : enum_item_struct -> Ppx_deriving_runtime.string
type enum_kind =
  1. | EKenum of longident
  2. | EKstate of namespace option
val show_enum_kind : enum_kind -> Ppx_deriving_runtime.string
type enum = {
  1. kind : enum_kind;
  2. items : enum_item_struct list;
  3. loc : Location.t;
}
type map_kind =
  1. | MKMap
  2. | MKBigMap
  3. | MKIterableBigMap
val show_map_kind : map_kind -> Ppx_deriving_runtime.string
type asset = {
  1. name : longident;
  2. fields : decl_gen list;
  3. keys : lident list;
  4. sort : lident list;
  5. map_kind : map_kind;
  6. state : lident option;
  7. init : pterm list list;
  8. specs : label_term list;
  9. loc : Location.t;
}
type position =
  1. | Pleaf of lident
  2. | Pnode of position list
val show_position : position -> Ppx_deriving_runtime.string
type record = {
  1. name : longident;
  2. fields : decl_gen list;
  3. pos : position;
  4. loc : Location.t;
}
val show_record : record -> Ppx_deriving_runtime.string
type decl_ =
  1. | Dvariable of variable
  2. | Dasset of asset
  3. | Drecord of record
  4. | Denum of enum
  5. | Devent of record
val pp_decl_ : Ppx_deriving_runtime.Format.formatter -> decl_ -> Ppx_deriving_runtime.unit
val show_decl_ : decl_ -> Ppx_deriving_runtime.string
type fun_ =
  1. | Ffunction of function_
  2. | Ftransaction of transaction
val pp_fun_ : Ppx_deriving_runtime.Format.formatter -> fun_ -> Ppx_deriving_runtime.unit
val show_fun_ : fun_ -> Ppx_deriving_runtime.string
type metadata_kind =
  1. | MKuri of string Location.loced
  2. | MKjson of string Location.loced
val show_metadata_kind : metadata_kind -> Ppx_deriving_runtime.string
type import_kind_node =
  1. | INMichelson of michelson_struct
  2. | INArchetype
val show_import_kind_node : import_kind_node -> Ppx_deriving_runtime.string
type import_struct = {
  1. name : lident;
  2. path : lident;
  3. kind_node : import_kind_node;
  4. views : (Ident.ident * (type_ * type_)) list;
  5. entrypoints : (Ident.ident * type_) list;
}
val show_import_struct : import_struct -> Ppx_deriving_runtime.string
type ast = {
  1. name : lident;
  2. parameters : parameter list;
  3. imports : import_struct list;
  4. metadata : metadata_kind option;
  5. decls : decl_ list;
  6. funs : fun_ list;
  7. specifications : specification list;
  8. securities : security list;
  9. loc : Location.t;
}
val vtaddress : ptyp
val vtbls12_381_fr : ptyp
val vtbls12_381_g1 : ptyp
val vtbls12_381_g2 : ptyp
val vtbool : ptyp
val vtbytes : ptyp
val vtchainid : ptyp
val vtcurrency : ptyp
val vtdate : ptyp
val vtduration : ptyp
val vtint : ptyp
val vtkey : ptyp
val vtkeyhash : ptyp
val vtnat : ptyp
val vtrational : ptyp
val vtsignature : ptyp
val vtstring : ptyp
val vtunit : ptyp
val vtnever : ptyp
val vtchest : ptyp
val vtchest_key : ptyp
val vttx_rollup_l2_address : ptyp
val vts : ptyp list
val mk_sp : ?label:Ident.ident -> ?loc:Location.t -> ?type_:type_ -> 'a -> 'a struct_poly
val mk_instr : ?label:string -> ?loc:Location.t -> instruction_node -> instruction
val mk_label_term : ?label:lident -> ?error:pterm -> ?loc:Location.t -> pterm -> label_term
val mk_variable : ?invs:label_term list -> ?loc:Location.t -> decl_gen -> variable_kind -> variable
val mk_predicate : ?args:(lident * type_) list -> ?loc:Location.t -> lident -> pterm -> predicate
val mk_definition : ?loc:Location.t -> lident -> type_ -> lident -> pterm -> definition
val mk_fail : ?loc:Location.t -> lident -> lident option -> lident -> type_ -> pterm -> fail
val mk_invariant : ?formulas:pterm list -> lident -> invariant
val mk_postcondition : ?invariants:invariant list -> ?uses:lident list -> lident -> pterm -> postcondition
val mk_assert : ?invariants:invariant list -> ?uses:lident list -> lident -> lident -> pterm -> assert_
val mk_specification : ?predicates:predicate list -> ?definitions:definition list -> ?fails:fail list -> ?lemmas:label_term list -> ?theorems:label_term list -> ?variables:variable list -> ?invariants:(lident * label_term list) list -> ?effect:instruction -> ?specs:postcondition list -> ?asserts:assert_ list -> ?loc:Location.t -> unit -> specification
val mk_function_struct : ?args:decl_gen list -> ?specification:specification -> ?loc:Location.t -> lident -> fun_kind -> instruction -> type_ -> function_
val mk_transition : ?on:(lident * type_ * lident * type_) -> ?trs:(lident * pterm option * instruction option) list -> sexpr -> transition
val mk_transaction_struct : ?args:decl_gen list -> ?sourcedby:(rexpr * pterm option) -> ?calledby:(rexpr * pterm option) -> ?state_is:(lident * pterm option) -> ?accept_transfer:(bool * pterm option) -> ?constants:label_term list -> ?require:label_term list -> ?failif:label_term list -> ?transition:transition -> ?specification:specification -> ?functions:function_ list -> ?effect:instruction -> ?loc:Location.t -> lident -> transaction
val mk_enum_item : ?initial:bool -> ?args:ptyp list -> ?invariants:label_term list -> ?loc:Location.t -> lident -> enum_item_struct
val mk_enum : ?items:enum_item_struct list -> ?loc:Location.t -> enum_kind -> enum
val mk_decl : ?typ:type_ -> ?default:pterm -> ?shadow:bool -> ?loc:Location.t -> lident -> decl_gen
val mk_asset : ?fields:decl_gen list -> ?keys:lident list -> ?sort:lident list -> ?map_kind:map_kind -> ?state:lident -> ?init:pterm list list -> ?specs:label_term list -> ?loc:Location.t -> longident -> asset
val mk_model : ?parameters:parameter list -> ?imports:import_struct list -> ?metadata:metadata_kind -> ?decls:decl_ list -> ?funs:fun_ list -> ?specifications:specification list -> ?securities:security list -> ?loc:Location.t -> lident -> ast
val mk_id : type_ -> lident -> qualid
val map_ptyp : (type_ -> type_) -> ptyp -> ptyp
module Utils : sig ... end
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct