package rocq-runtime

  1. Overview
  2. Docs
The Rocq Prover -- Core Binaries and Tools

Install

Dune Dependency

rocq-prover.org Readme Edit opam file Versions (1)

Authors

  1. T
    The Rocq development team, INRIA, CNRS, and contributors

Maintainers

  1. T
    The Rocq development team <coqdev@inria.fr>

Sources

rocq-9.0.0.tar.gz
md5=8d522602d23e7a665631826dab9aa92b
sha512=f4f76a6a178e421c99ee7a331a2fd97a06e9c5d0168d7e60c44e3820d8e1a124370ea104ad90c7f87a9a1e9d87b2d0d7d2d387c998feeaed4a75ed04e176a4be

doc/ssreflect_plugin/Ssreflect_plugin/Ssrast/index.html

Module Ssreflect_plugin.Ssrast

type ssrhyp =
  1. | SsrHyp of Names.Id.t Loc.located
type 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 =
  1. | Simpl of int
  2. | Cut of int
  3. | SimplCut of int * int
  4. | Nop
type ssrmmod =
  1. | May
  2. | Must
  3. | Once
type ssrmult = int * ssrmmod
type ssrocc = (bool * int list) option

Occurrence switch

2

, all is Some(false,)

type ssrindex = int Locus.or_var
type ssrclear = ssrhyps
type ssrdocc = ssrclear option * ssrocc
type 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 = {
  1. body : Constrexpr.constr_expr;
  2. glob_env : ast_glob_env option;
  3. interp_env : Geninterp.interp_sign option;
  4. annotation : [ `None | `Parens | `DoubleParens | `At ];
}
type ssrview = ast_closure_term list
type id_block =
  1. | Prefix of Names.Id.t
  2. | SuffixId of Names.Id.t
  3. | SuffixNum of int
type anon_kind =
  1. | One of string option
  2. | Drop
  3. | All
  4. | Temporary
type 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 =
  1. | Block of id_block
  2. | Regular of ssripats list
type ssrhpats = ((ssrclear option * ssripats) * ssripats) * ssripats
type ssrhpats_wtransp = bool * ssrhpats
type ssrfwdid = Names.Id.t
type 'term 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

Binders (for fwd tactics)

type 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 =
  1. | FwdHint of string * bool
  2. | FwdHave
  3. | FwdPose

Forward chaining argument

type ssrfwdfmt = ssrfwdkind * ssrbindfmt list
type 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 'a ssragens = (ssrdocc * 'a) list list * ssrclear
type ssrapplyarg = ssrterm list * (ssrterm ssragens * ssripats)
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