package rocq-runtime

  1. Overview
  2. Docs
package rocq-runtime
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module VernactypesSource

Interpretation of extended vernac phrases.

Sourcemodule Prog : sig ... end
Sourcemodule Proof : sig ... end
Sourcemodule OpaqueAccess : sig ... end
Sourcetype ('prog, 'proof, 'opaque_access) state_gen = {
  1. prog : 'prog;
  2. proof : 'proof;
  3. opaque_access : 'opaque_access;
}
Sourcetype no_state = (unit, unit, unit) state_gen
Sourceval no_state : no_state

Useful for patterns like { no_state with proof = newproof } when modifying a subset of the state.

Sourceval ignore_state : ((unit, unit) Prog.t, (unit, unit) Proof.t, unit OpaqueAccess.t) state_gen
Sourcetype 'r typed_vernac_gen =
  1. | TypedVernac : {
    1. spec : (('inprog, 'outprog) Prog.t, ('inproof, 'outproof) Proof.t, 'inaccess OpaqueAccess.t) state_gen;
    2. run : ('inprog, 'inproof, 'inaccess) state_gen -> ('outprog, 'outproof, unit) state_gen * 'r;
    } -> 'r typed_vernac_gen
Sourcetype typed_vernac = unit typed_vernac_gen
Sourceval typed_vernac_gen : (('inprog, 'outprog) Prog.t, ('inproof, 'outproof) Proof.t, 'inaccess OpaqueAccess.t) state_gen -> (('inprog, 'inproof, 'inaccess) state_gen -> ('outprog, 'outproof, unit) state_gen * 'r) -> 'r typed_vernac_gen
Sourceval map_typed_vernac : ('a -> 'b) -> 'a typed_vernac_gen -> 'b typed_vernac_gen
Sourceval typed_vernac : (('inprog, 'outprog) Prog.t, ('inproof, 'outproof) Proof.t, 'inaccess OpaqueAccess.t) state_gen -> (('inprog, 'inproof, 'inaccess) state_gen -> ('outprog, 'outproof, unit) state_gen) -> typed_vernac
Sourcetype full_state = (Prog.stack, Vernacstate.LemmaStack.t option, unit) state_gen

Some convenient typed_vernac constructors. Used by coqpp.

Sourceval vtdefault : (unit -> unit) -> typed_vernac
Sourceval vtnoproof : (unit -> unit) -> typed_vernac
Sourceval vtopenproof : (unit -> Declare.Proof.t) -> typed_vernac
Sourceval vtmodifyproof : (pstate:Declare.Proof.t -> Declare.Proof.t) -> typed_vernac
Sourceval vtreadproofopt : (pstate:Declare.Proof.t option -> unit) -> typed_vernac
Sourceval vtreadproof : (pstate:Declare.Proof.t -> unit) -> typed_vernac
Sourceval vtreadprogram : (pm:Declare.OblState.t -> unit) -> typed_vernac
Sourceval vtdeclareprogram : (pm:Declare.OblState.t -> Declare.Proof.t) -> typed_vernac
Sourceval vtopaqueaccess : (opaque_access:Global.indirect_accessor -> unit) -> typed_vernac
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