To focus the search input from anywhere on the page, press the 'S' key.
in-package search v0.1.0
Legend:
Library
Module
Module type
Parameter
Class
Class type
Library
Module
Module type
Parameter
Class
Class type
module Loc = Serlib.Ser_loc
module Names = Serlib.Ser_names
module Locus = Serlib.Ser_locus
module Constrexpr = Serlib.Ser_constrexpr
module Genintern = Serlib.Ser_genintern
module Geninterp = Serlib.Ser_geninterp
module Ssrmatching_plugin : sig ... end
module Ltac_plugin : sig ... end
type ssrtermkind = Ssrmatching_plugin.Ssrmatching.ssrtermkind
val ssrtermkind_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> ssrtermkind
val sexp_of_ssrtermkind : ssrtermkind -> Ppx_sexp_conv_lib.Sexp.t
module Proofview : sig ... end
val ssrhyp_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> ssrhyp
val sexp_of_ssrhyp : ssrhyp -> Ppx_sexp_conv_lib.Sexp.t
val ssrhyp_or_id_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> ssrhyp_or_id
val sexp_of_ssrhyp_or_id : ssrhyp_or_id -> Ppx_sexp_conv_lib.Sexp.t
type ssrhyps = ssrhyp list
val ssrhyps_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> ssrhyps
val sexp_of_ssrhyps : ssrhyps -> Ppx_sexp_conv_lib.Sexp.t
val ssrdir_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> ssrdir
val sexp_of_ssrdir : ssrdir -> Ppx_sexp_conv_lib.Sexp.t
val ssrsimpl_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> ssrsimpl
val sexp_of_ssrsimpl : ssrsimpl -> Ppx_sexp_conv_lib.Sexp.t
val ssrmmod_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> ssrmmod
val sexp_of_ssrmmod : ssrmmod -> Ppx_sexp_conv_lib.Sexp.t
type ssrmult = int * ssrmmod
val ssrmult_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> ssrmult
val sexp_of_ssrmult : ssrmult -> Ppx_sexp_conv_lib.Sexp.t
val ssrocc_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> ssrocc
val sexp_of_ssrocc : ssrocc -> Ppx_sexp_conv_lib.Sexp.t
type ssrindex = int Locus.or_var
val ssrindex_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> ssrindex
val sexp_of_ssrindex : ssrindex -> Ppx_sexp_conv_lib.Sexp.t
type ssrclear = ssrhyps
val ssrclear_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> ssrclear
val sexp_of_ssrclear : ssrclear -> Ppx_sexp_conv_lib.Sexp.t
val ssrdocc_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> ssrdocc
val sexp_of_ssrdocc : ssrdocc -> Ppx_sexp_conv_lib.Sexp.t
type ssrterm = ssrtermkind * Genintern.glob_constr_and_expr
val ssrterm_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> ssrterm
val sexp_of_ssrterm : ssrterm -> Ppx_sexp_conv_lib.Sexp.t
type ast_glob_env = {
ast_ltacvars : Names.Id.Set.t;
ast_extra : Genintern.Store.t;
ast_intern_sign : Genintern.intern_variable_status;
}
val ast_glob_env_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> ast_glob_env
val sexp_of_ast_glob_env : ast_glob_env -> Ppx_sexp_conv_lib.Sexp.t
type ast_closure_term = {
body : Constrexpr.constr_expr;
glob_env : ast_glob_env option;
interp_env : Geninterp.interp_sign option;
annotation : [ `At | `DoubleParens | `Parens | `None ];
}
val ast_closure_term_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> ast_closure_term
val sexp_of_ast_closure_term : ast_closure_term -> Ppx_sexp_conv_lib.Sexp.t
type ssrview = ast_closure_term list
val ssrview_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> ssrview
val sexp_of_ssrview : ssrview -> Ppx_sexp_conv_lib.Sexp.t
val anon_kind_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> anon_kind
val sexp_of_anon_kind : anon_kind -> Ppx_sexp_conv_lib.Sexp.t
val id_block_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> id_block
val sexp_of_id_block : id_block -> Ppx_sexp_conv_lib.Sexp.t
type ssripat =
| IPatNoop
| IPatId of Names.Id.t
| IPatAnon of anon_kind
| IPatDispatch of ssripatss_or_block
| IPatCase of ssripatss_or_block
| IPatInj of ssripatss
| IPatRewrite of ssrocc * ssrdir
| IPatView of ssrview
| IPatClear of ssrclear
| IPatSimpl of ssrsimpl
| IPatAbstractVars of Names.Id.t list
| IPatFastNondep
and ssripats = ssripat list
and ssripatss = ssripats list
val ssripat_of_sexp : Sexplib0.Sexp.t -> ssripat
val ssripats_of_sexp : Sexplib0.Sexp.t -> ssripats
val ssripatss_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> ssripatss
val ssripatss_or_block_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> ssripatss_or_block
val sexp_of_ssripat : ssripat -> Sexplib0.Sexp.t
val sexp_of_ssripats : ssripats -> Sexplib0.Sexp.t
val sexp_of_ssripatss : ssripatss -> Ppx_sexp_conv_lib.Sexp.t
val sexp_of_ssripatss_or_block : ssripatss_or_block -> Ppx_sexp_conv_lib.Sexp.t
val ssrhpats_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> ssrhpats
val sexp_of_ssrhpats : ssrhpats -> Ppx_sexp_conv_lib.Sexp.t
type ssrhpats_wtransp = bool * ssrhpats
val ssrhpats_wtransp_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> ssrhpats_wtransp
val sexp_of_ssrhpats_wtransp : ssrhpats_wtransp -> Ppx_sexp_conv_lib.Sexp.t
type ssrintrosarg = Ltac_plugin.Tacexpr.raw_tactic_expr * ssripats
val ssrintrosarg_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> ssrintrosarg
val sexp_of_ssrintrosarg : ssrintrosarg -> Ppx_sexp_conv_lib.Sexp.t
type ssrfwdid = Names.Id.t
val ssrfwdid_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> ssrfwdid
val sexp_of_ssrfwdid : ssrfwdid -> Ppx_sexp_conv_lib.Sexp.t
type 'term ssrbind =
| Bvar of Names.Name.t
| Bdecl of Names.Name.t list * 'term
| Bdef of Names.Name.t * 'term option * 'term
| Bstruct of Names.Name.t
| Bcast of 'term
val ssrbind_of_sexp :
'term. (Ppx_sexp_conv_lib.Sexp.t -> 'term) ->
Ppx_sexp_conv_lib.Sexp.t ->
'term ssrbind
val sexp_of_ssrbind :
'term. ('term -> Ppx_sexp_conv_lib.Sexp.t) ->
'term ssrbind ->
Ppx_sexp_conv_lib.Sexp.t
val ssrbindfmt_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> ssrbindfmt
val sexp_of_ssrbindfmt : ssrbindfmt -> Ppx_sexp_conv_lib.Sexp.t
type 'term ssrbindval = 'term ssrbind list * 'term
val ssrbindval_of_sexp :
'term. (Ppx_sexp_conv_lib.Sexp.t -> 'term) ->
Ppx_sexp_conv_lib.Sexp.t ->
'term ssrbindval
val sexp_of_ssrbindval :
'term. ('term -> Ppx_sexp_conv_lib.Sexp.t) ->
'term ssrbindval ->
Ppx_sexp_conv_lib.Sexp.t
val ssrfwdkind_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> ssrfwdkind
val sexp_of_ssrfwdkind : ssrfwdkind -> Ppx_sexp_conv_lib.Sexp.t
type ssrfwdfmt = ssrfwdkind * ssrbindfmt list
val ssrfwdfmt_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> ssrfwdfmt
val sexp_of_ssrfwdfmt : ssrfwdfmt -> Ppx_sexp_conv_lib.Sexp.t
val ssrclseq_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> ssrclseq
val sexp_of_ssrclseq : ssrclseq -> Ppx_sexp_conv_lib.Sexp.t
val ssrhint_of_sexp :
'tac. (Ppx_sexp_conv_lib.Sexp.t -> 'tac) ->
Ppx_sexp_conv_lib.Sexp.t ->
'tac ssrhint
val sexp_of_ssrhint :
'tac. ('tac -> Ppx_sexp_conv_lib.Sexp.t) ->
'tac ssrhint ->
Ppx_sexp_conv_lib.Sexp.t
type 'tac fwdbinders =
bool * (ssrhpats * ((ssrfwdfmt * ast_closure_term) * 'tac ssrhint))
val fwdbinders_of_sexp :
'tac. (Ppx_sexp_conv_lib.Sexp.t -> 'tac) ->
Ppx_sexp_conv_lib.Sexp.t ->
'tac fwdbinders
val sexp_of_fwdbinders :
'tac. ('tac -> Ppx_sexp_conv_lib.Sexp.t) ->
'tac fwdbinders ->
Ppx_sexp_conv_lib.Sexp.t
type 'tac ffwbinders =
ssrhpats * ((ssrfwdfmt * ast_closure_term) * 'tac ssrhint)
val ffwbinders_of_sexp :
'tac. (Ppx_sexp_conv_lib.Sexp.t -> 'tac) ->
Ppx_sexp_conv_lib.Sexp.t ->
'tac ffwbinders
val sexp_of_ffwbinders :
'tac. ('tac -> Ppx_sexp_conv_lib.Sexp.t) ->
'tac ffwbinders ->
Ppx_sexp_conv_lib.Sexp.t
type clause =
ssrclear
* ((ssrhyp_or_id * string) * Ssrmatching_plugin.Ssrmatching.cpattern option)
option
val clause_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> clause
val sexp_of_clause : clause -> Ppx_sexp_conv_lib.Sexp.t
val clauses_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> clauses
val sexp_of_clauses : clauses -> Ppx_sexp_conv_lib.Sexp.t
type wgen =
ssrclear
* ((ssrhyp_or_id * string) * Ssrmatching_plugin.Ssrmatching.cpattern option)
option
val wgen_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> wgen
val sexp_of_wgen : wgen -> Ppx_sexp_conv_lib.Sexp.t
val ssrdoarg_of_sexp :
'a. (Ppx_sexp_conv_lib.Sexp.t -> 'a) ->
Ppx_sexp_conv_lib.Sexp.t ->
'a ssrdoarg
val sexp_of_ssrdoarg :
'a. ('a -> Ppx_sexp_conv_lib.Sexp.t) ->
'a ssrdoarg ->
Ppx_sexp_conv_lib.Sexp.t
val ssrseqarg_of_sexp :
'a. (Ppx_sexp_conv_lib.Sexp.t -> 'a) ->
Ppx_sexp_conv_lib.Sexp.t ->
'a ssrseqarg
val sexp_of_ssrseqarg :
'a. ('a -> Ppx_sexp_conv_lib.Sexp.t) ->
'a ssrseqarg ->
Ppx_sexp_conv_lib.Sexp.t
val ssragens_of_sexp :
'a. (Ppx_sexp_conv_lib.Sexp.t -> 'a) ->
Ppx_sexp_conv_lib.Sexp.t ->
'a ssragens
val sexp_of_ssragens :
'a. ('a -> Ppx_sexp_conv_lib.Sexp.t) ->
'a ssragens ->
Ppx_sexp_conv_lib.Sexp.t
val ssrapplyarg_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> ssrapplyarg
val sexp_of_ssrapplyarg : ssrapplyarg -> Ppx_sexp_conv_lib.Sexp.t
val ssrcasearg_of_sexp :
'a. (Ppx_sexp_conv_lib.Sexp.t -> 'a) ->
Ppx_sexp_conv_lib.Sexp.t ->
'a ssrcasearg
val sexp_of_ssrcasearg :
'a. ('a -> Ppx_sexp_conv_lib.Sexp.t) ->
'a ssrcasearg ->
Ppx_sexp_conv_lib.Sexp.t
type 'a ssrmovearg = ssrview * 'a ssrcasearg
val ssrmovearg_of_sexp :
'a. (Ppx_sexp_conv_lib.Sexp.t -> 'a) ->
Ppx_sexp_conv_lib.Sexp.t ->
'a ssrmovearg
val sexp_of_ssrmovearg :
'a. ('a -> Ppx_sexp_conv_lib.Sexp.t) ->
'a ssrmovearg ->
Ppx_sexp_conv_lib.Sexp.t
sectionYPositions = computeSectionYPositions($el), 10)"
x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
>