package rocq-runtime

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

Install 

dune-project
 Dependency

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

Authors

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

Maintainers

  1. T
    The Rocq development team <rocq+rocq-development@discoursemail.com>

Sources

rocq-9.1.0.tar.gz
sha256=b236dc44f92e1eeca6877c7ee188a90c2303497fe7beb99df711ed5a7ce0d824

doc/rocq-runtime.checklib/Coq_checklib/Analyze/index.html

Module Coq_checklib.AnalyzeSource

Sourcetype data =
  1. | Int of int
  2. | Ptr of int
  3. | Atm of int
  4. | Fun of int

Representation of data allocated on the OCaml heap.

Sourcetype obj =
  1. | Struct of int * data array
  2. | Int64 of Int64.t
  3. | Float64 of float
  4. | String of string
Sourcemodule LargeArray : sig ... end

A data structure similar to arrays but allowing to overcome the 2^22 length limitation on 32-bit architecture.

Sourceval parse_channel : in_channel -> data * obj LargeArray.t
Sourceval parse_string : string -> data * obj LargeArray.t
Functorized version
Sourcemodule type Input = sig ... end

Type of inputs

Sourcemodule type S = sig ... end
Sourcemodule Make (M : Input) : S with type input = M.t

Functorized version of the previous code.

Sourceval instantiate : (data * obj LargeArray.t) -> Obj.t

Create the OCaml object out of the reified representation.