package coq-serapi
Serialization library and protocol for machine interaction with the Coq proof assistant
Install
Dune Dependency
Authors
Maintainers
Sources
coq-serapi-8.17.0.0.17.2.tbz
sha256=33df78ad19b46d8f3719e54bbee3047d72e1e7fa63399b7ede4d049a08b41c53
sha512=2dafee85729b80f15e8bab167a21290bba43d0c6d34476dd2afa42ebb2ef6dca353a0d2291db6a0cdafc4923e878b508e01ac0660e2eefb211cbc03d53f5ba4d
doc/serlib_ltac2/Serlib_ltac2/Ser_tac2expr/index.html
Module Serlib_ltac2.Ser_tac2expr
Source
module Loc = Serlib.Ser_loc
module CAst = Serlib.Ser_cAst
module Names = Serlib.Ser_names
module Libnames = Serlib.Ser_libnames
Source
val mutable_flag_of_yojson :
Yojson.Safe.t ->
mutable_flag Ppx_deriving_yojson_runtime.error_or
Source
val hash_fold_mutable_flag :
Ppx_hash_lib.Std.Hash.state ->
mutable_flag ->
Ppx_hash_lib.Std.Hash.state
Source
val hash_fold_redef_flag :
Ppx_hash_lib.Std.Hash.state ->
redef_flag ->
Ppx_hash_lib.Std.Hash.state
Source
type 'a or_relid = 'a Ltac2_plugin.Tac2expr.or_relid =
| RelId of Libnames.qualid
| AbsKn of 'a
Source
val type_constant_of_yojson :
Yojson.Safe.t ->
type_constant Ppx_deriving_yojson_runtime.error_or
Source
val hash_fold_type_constant :
Ppx_hash_lib.Std.Hash.state ->
type_constant ->
Ppx_hash_lib.Std.Hash.state
Source
type raw_typexpr_r = Ltac2_plugin.Tac2expr.raw_typexpr_r =
| CTypVar of Names.Name.t
| CTypArrow of raw_typexpr * raw_typexpr
| CTypRef of type_constant or_tuple or_relid * raw_typexpr list
Source
val raw_typexpr_r_of_yojson :
Yojson.Safe.t ->
raw_typexpr_r Ppx_deriving_yojson_runtime.error_or
Source
type raw_typedef = Ltac2_plugin.Tac2expr.raw_typedef =
| CTydDef of raw_typexpr option
| CTydAlg of (uid * raw_typexpr list) list
| CTydRec of (lid * mutable_flag * raw_typexpr) list
| CTydOpn
Source
val hash_fold_raw_typedef :
Ppx_hash_lib.Std.Hash.state ->
raw_typedef ->
Ppx_hash_lib.Std.Hash.state
Source
val raw_quant_typedef_of_yojson :
Yojson.Safe.t ->
raw_quant_typedef Ppx_deriving_yojson_runtime.error_or
Source
val hash_fold_raw_quant_typedef :
Ppx_hash_lib.Std.Hash.state ->
raw_quant_typedef ->
Ppx_hash_lib.Std.Hash.state
Source
val ltac_constant_of_yojson :
Yojson.Safe.t ->
ltac_constant Ppx_deriving_yojson_runtime.error_or
Source
val hash_fold_ltac_constant :
Ppx_hash_lib.Std.Hash.state ->
ltac_constant ->
Ppx_hash_lib.Std.Hash.state
Source
val hash_fold_ltac_alias :
Ppx_hash_lib.Std.Hash.state ->
ltac_alias ->
Ppx_hash_lib.Std.Hash.state
Source
val ltac_constructor_of_yojson :
Yojson.Safe.t ->
ltac_constructor Ppx_deriving_yojson_runtime.error_or
Source
val hash_fold_ltac_constructor :
Ppx_hash_lib.Std.Hash.state ->
ltac_constructor ->
Ppx_hash_lib.Std.Hash.state
Source
val ltac_projection_of_yojson :
Yojson.Safe.t ->
ltac_projection Ppx_deriving_yojson_runtime.error_or
Source
val hash_fold_ltac_projection :
Ppx_hash_lib.Std.Hash.state ->
ltac_projection ->
Ppx_hash_lib.Std.Hash.state
Source
and raw_patexpr_r = Ltac2_plugin.Tac2expr.raw_patexpr_r =
| CPatVar of Names.Name.t
| CPatAtm of atom
| CPatRef of ltac_constructor or_tuple or_relid * raw_patexpr list
| CPatRecord of (ltac_projection or_relid * raw_patexpr) list
| CPatCnv of raw_patexpr * raw_typexpr
| CPatOr of raw_patexpr list
| CPatAs of raw_patexpr * Names.lident
Source
val raw_patexpr_r_of_yojson :
Yojson.Safe.t ->
raw_patexpr_r Ppx_deriving_yojson_runtime.error_or
Source
type tacref = Ltac2_plugin.Tac2expr.tacref =
| TacConstant of ltac_constant
| TacAlias of ltac_alias
module Obj : sig ... end
module T2E : sig ... end
Source
val raw_tacexpr_r_of_yojson :
Yojson.Safe.t ->
raw_tacexpr_r Ppx_deriving_yojson_runtime.error_or
Source
val hash_fold_raw_tacexpr_r :
Ppx_hash_lib.Std.Hash.state ->
raw_tacexpr_r ->
Ppx_hash_lib.Std.Hash.state
Source
val hash_fold_raw_tacexpr :
Ppx_hash_lib.Std.Hash.state ->
raw_tacexpr ->
Ppx_hash_lib.Std.Hash.state
Source
val ml_tactic_name_of_yojson :
Yojson.Safe.t ->
ml_tactic_name Ppx_deriving_yojson_runtime.error_or
Source
val hash_fold_ml_tactic_name :
Ppx_hash_lib.Std.Hash.state ->
ml_tactic_name ->
Ppx_hash_lib.Std.Hash.state
Source
type strexpr = Ltac2_plugin.Tac2expr.strexpr =
| StrVal of mutable_flag * rec_flag * (Names.lname * raw_tacexpr) list
| StrTyp of rec_flag * (Libnames.qualid * redef_flag * raw_quant_typedef) list
| StrPrm of Names.lident * raw_typexpr * ml_tactic_name
| StrSyn of sexpr list * int option * raw_tacexpr
| StrMut of Libnames.qualid * Names.lident option * raw_tacexpr
Source
type 'a open_match = 'a Ltac2_plugin.Tac2expr.open_match = {
opn_match : 'a;
opn_branch : (Names.Name.t * Names.Name.t array * 'a) Names.KNmap.t;
opn_default : Names.Name.t * 'a;
}
Source
val open_match_of_yojson :
'a. (Yojson.Safe.t -> 'a Ppx_deriving_yojson_runtime.error_or) ->
Yojson.Safe.t ->
'a open_match Ppx_deriving_yojson_runtime.error_or
Source
val hash_fold_open_match :
'a. (Ppx_hash_lib.Std.Hash.state -> 'a -> Ppx_hash_lib.Std.Hash.state) ->
Ppx_hash_lib.Std.Hash.state ->
'a open_match ->
Ppx_hash_lib.Std.Hash.state
module GT2E : sig ... end
Source
val hash_fold_glb_tacexpr :
Ppx_hash_lib.Std.Hash.state ->
glb_tacexpr ->
Ppx_hash_lib.Std.Hash.state
sectionYPositions = computeSectionYPositions($el), 10)"
x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
>