package rocq-runtime
The Rocq Prover -- Core Binaries and Tools
Install
Dune Dependency
Authors
Maintainers
Sources
rocq-9.0.0.tar.gz
md5=8d522602d23e7a665631826dab9aa92b
sha512=f4f76a6a178e421c99ee7a331a2fd97a06e9c5d0168d7e60c44e3820d8e1a124370ea104ad90c7f87a9a1e9d87b2d0d7d2d387c998feeaed4a75ed04e176a4be
doc/ssreflect_plugin/Ssreflect_plugin/Ssripats/index.html
Module Ssreflect_plugin.SsripatsSource
Source
type ssriop = | IOpId of Names.Id.t| IOpDrop| IOpTemporay| IOpInaccessible of string option| IOpInaccessibleAll| IOpAbstractVars of Names.Id.t list| IOpFastNondep| IOpInj of ssriops list| IOpDispatchBlock of Ssrast.id_block| IOpDispatchBranches of ssriops list| IOpCaseBlock of Ssrast.id_block| IOpCaseBranches of ssriops list| IOpRewrite of Ssrast.ssrocc * Ssrast.ssrdir| IOpView of Ssrast.ssrclear option * Ssrast.ssrview| IOpClear of Ssrast.ssrclear * Ssrast.ssrhyp option| IOpSimpl of Ssrast.ssrsimpl| IOpEqGen of unit Proofview.tactic| IOpNoop