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.0.1.tar.gz
sha256=051f7bf702ff0a3b370449728921e5a95e18bc2b31b8eb949d48422888c98af4

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.