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/Values/index.html

Module Coq_checklib.ValuesSource

Sourcetype 'v kind = private
  1. | Any
    (*

    A value that we won't check,

    *)
  2. | Fail of string
    (*

    A value that shouldn't be there at all,

    *)
  3. | Tuple of string * 'v array
    (*

    A debug name and sub-values in this block

    *)
  4. | Sum of string * int * 'v array array
    (*

    A debug name, a number of constant constructors, and sub-values at each position of each possible constructed variant

    *)
  5. | Array of 'v
  6. | List of 'v
  7. | Opt of 'v
  8. | Int
  9. | String
    (*

    Builtin Ocaml types.

    *)
  10. | Annot of string * 'v
    (*

    Adds a debug note to the inner value

    *)
  11. | Int64
  12. | Float64
Sourcetype value
Sourceval equal : value -> value -> bool
Sourceval kind : value -> value kind
Sourceval v_any : value
Sourceval v_fail : string -> value
Sourceval v_tuple : string -> value array -> value
Sourceval v_sum : string -> int -> value array array -> value
Sourceval v_array : value -> value
Sourceval v_list : value -> value
Sourceval v_opt : value -> value
Sourceval v_int : value
Sourceval v_string : value
Sourceval v_annot : string -> value -> value
Sourceval v_int64 : value
Sourceval v_float64 : value
Sourceval fix : (value -> value) -> value

Define a recursive value. fix (fun v -> v) is invalid.

Sourceval v_libsum : value
Sourceval v_lib : value
Sourceval v_opaquetable : value
Sourceval v_vmlib : value