package coq-serapi

  1. Overview
  2. Docs
Serialization library and protocol for machine interaction with the Coq proof assistant

Install

Dune Dependency

github.com Readme Changelog Edit opam file Versions (38)

Authors

  1. E
    Emilio Jesús Gallego Arias
  2. K
    Karl Palmskog
  3. C
    Clément Pit-Claudel
  4. K
    Kaiyu Yang

Maintainers

  1. E
    e@x80.org

Sources

coq-serapi-8.16.0.0.16.2.tbz
sha256=f891507f58fba3ba29889dd07fbe69af3411d246488ae7595cd81d26c8422f14
sha512=224dfda8fae1ead7a5ae2a8ead527834bb5216b1788485a0c19deade3b0dd86767c19056931294a7973f132680e282c4491c76ef38638c0c566a029379f484e2

doc/serlib_ssr/Serlib_ssr/Wrap_ssrast/Wrap/index.html

Module Wrap_ssrast.WrapSource

include module type of Ssreflect_plugin.Ssrast
type ssrhyp = Ssreflect_plugin__Ssrast.ssrhyp =
  1. | SsrHyp of Names.Id.t Loc.located
type ssrhyp_or_id = Ssreflect_plugin__Ssrast.ssrhyp_or_id =
  1. | Hyp of ssrhyp
  2. | Id of ssrhyp
type ssrhyps = ssrhyp list
type ssrdir = Ssrmatching_plugin.Ssrmatching.ssrdir =
  1. | L2R
  2. | R2L
type ssrsimpl = Ssreflect_plugin__Ssrast.ssrsimpl =
  1. | Simpl of int
  2. | Cut of int
  3. | SimplCut of int * int
  4. | Nop
type ssrmmod = Ssreflect_plugin__Ssrast.ssrmmod =
  1. | May
  2. | Must
  3. | Once
type ssrmult = int * ssrmmod
type ssrocc = (bool * int list) option
type ssrindex = int Locus.or_var
type ssrclear = ssrhyps
type ssrdocc = ssrclear option * ssrocc
type ssrtermkind = Ssrmatching_plugin.Ssrmatching.ssrtermkind
type ssrterm = ssrtermkind * Genintern.glob_constr_and_expr
type ast_glob_env = Ssreflect_plugin__Ssrast.ast_glob_env = {
  1. ast_ltacvars : Names.Id.Set.t;
  2. ast_extra : Genintern.Store.t;
  3. ast_intern_sign : Genintern.intern_variable_status;
}
type ast_closure_term = Ssreflect_plugin__Ssrast.ast_closure_term = {
  1. body : Constrexpr.constr_expr;
  2. glob_env : ast_glob_env option;
  3. interp_env : Geninterp.interp_sign option;
  4. annotation : [ `At | `DoubleParens | `None | `Parens ];
}
type ssrview = ast_closure_term list
type id_block = Ssreflect_plugin__Ssrast.id_block =
  1. | Prefix of Names.Id.t
  2. | SuffixId of Names.Id.t
  3. | SuffixNum of int
type anon_kind = Ssreflect_plugin__Ssrast.anon_kind =
  1. | One of string option
  2. | Drop
  3. | All
  4. | Temporary
type ssripat = Ssreflect_plugin__Ssrast.ssripat =
  1. | IPatNoop
  2. | IPatId of Names.Id.t
  3. | IPatAnon of anon_kind
  4. | IPatDispatch of ssripatss_or_block
  5. | IPatCase of ssripatss_or_block
  6. | IPatInj of ssripatss
  7. | IPatRewrite of ssrocc * ssrdir
  8. | IPatView of ssrview
  9. | IPatClear of ssrclear
  10. | IPatSimpl of ssrsimpl
  11. | IPatAbstractVars of Names.Id.t list
  12. | IPatFastNondep
and ssripats = ssripat list
and ssripatss = ssripats list
and ssripatss_or_block = Ssreflect_plugin__Ssrast.ssripatss_or_block =
  1. | Block of id_block
  2. | Regular of ssripats list
type ssrhpats = ((ssrclear option * ssripats) * ssripats) * ssripats
type ssrhpats_wtransp = bool * ssrhpats
type ssrintrosarg = Ltac_plugin.Tacexpr.raw_tactic_expr * ssripats
type ssrfwdid = Names.Id.t
type !'term ssrbind = 'term Ssreflect_plugin__Ssrast.ssrbind =
  1. | Bvar of Names.Name.t
  2. | Bdecl of Names.Name.t list * 'term
  3. | Bdef of Names.Name.t * 'term option * 'term
  4. | Bstruct of Names.Name.t
  5. | Bcast of 'term
type ssrbindfmt = Ssreflect_plugin__Ssrast.ssrbindfmt =
  1. | BFvar
  2. | BFdecl of int
  3. | BFcast
  4. | BFdef
  5. | BFrec of bool * bool
type !'term ssrbindval = 'term ssrbind list * 'term
type ssrfwdkind = Ssreflect_plugin__Ssrast.ssrfwdkind =
  1. | FwdHint of string * bool
  2. | FwdHave
  3. | FwdPose
type ssrfwdfmt = ssrfwdkind * ssrbindfmt list
type ssrclseq = Ssreflect_plugin__Ssrast.ssrclseq =
  1. | InGoal
  2. | InHyps
  3. | InHypsGoal
  4. | InHypsSeqGoal
  5. | InSeqGoal
  6. | InHypsSeq
  7. | InAll
  8. | InAllHyps
type !'tac ssrhint = bool * 'tac option list
type !'tac fwdbinders = bool * (ssrhpats * ((ssrfwdfmt * ast_closure_term) * 'tac ssrhint))
type !'tac ffwbinders = ssrhpats * ((ssrfwdfmt * ast_closure_term) * 'tac ssrhint)
type clause = ssrclear * ((ssrhyp_or_id * string) * Ssrmatching_plugin.Ssrmatching.cpattern option) option
type clauses = clause list * ssrclseq
type wgen = ssrclear * ((ssrhyp_or_id * string) * Ssrmatching_plugin.Ssrmatching.cpattern option) option
type !'a ssrdoarg = ((ssrindex * ssrmmod) * 'a ssrhint) * clauses
type !'a ssrseqarg = ssrindex * ('a ssrhint * 'a option)
type !'a ssrcasearg = ssripat option * ('a * ssripats)
type !'a ssrmovearg = ssrview * 'a ssrcasearg
type ssrdgens = Ssreflect_plugin__Ssrast.ssrdgens = {
  1. dgens : (ssrdocc * Ssrmatching_plugin.Ssrmatching.cpattern) list;
  2. gens : (ssrdocc * Ssrmatching_plugin.Ssrmatching.cpattern) list;
  3. clr : ssrclear;
}
type !'a ssragens = (ssrdocc * 'a) list list * ssrclear
type ssrapplyarg = ssrterm list * (ssrterm ssragens * ssripats)
type gist = Ltac_plugin.Tacintern.glob_sign
type ist = Ltac_plugin.Tacinterp.interp_sign
type goal = Evar.t
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