package ortac-qcheck-stm

  1. Overview
  2. Docs
Legend:
Library
Module
Module type
Parameter
Class
Class type
module Cfg = Config
val ty_default : Ppxlib.core_type_desc
val res_default : Ident.t
val may_raise_exception : Ir.value -> bool
val list_fold_right1 : ('a -> 'a -> 'a) -> 'a -> 'a list -> 'a
val qualify : string list -> string -> Astlib.Ast_500.Parsetree.expression
val subst_core_type : (string * Ppxlib.core_type) list -> Ppxlib.core_type -> Ppxlib.core_type
val subst_term : (Gospel.Tterm.Ident.t * 'a) list -> gos_t:Gospel.Tterm.Ident.t -> ?old_lz:bool -> old_t:Gospel.Symbols.Ident.t option -> ?new_lz:bool -> new_t:Gospel.Symbols.Ident.t option -> Gospel.Tterm.term -> Gospel.Tterm.term Reserr.reserr

subst_term state ~gos_t ?old_lz ~old_t ?new_lz ~new_t trm will substitute occurrences of gos_t with new_t or old_t depending on whether the occurrence appears above or under the old operator, adding a Lazy.force if the corresponding xxx_lz is true (defaults to false). gos_t must always be in a position in which it is applied to one of its model fields. Calling subst_term with new_t and old_t as None will check that the term does not contain gos_t

val str_of_ident : Ident.t -> string
val longident_loc_of_ident : Ident.t -> Ppxlib.longident Ppxlib.loc
val next_state_case : (Gospel.Tterm.Ident.t * 'a) list -> Cfg.t -> Ident.t -> int -> Ir.value -> (int list * Astlib.Ast_500.Parsetree.case) Reserr.reserr
val ghost_functions : Cfg.t -> Gospel.Tast.function_ list -> (Cfg.t * Ppxlib.structure_item list) Reserr.reserr
OCaml

Innovation. Community. Security.