package coq-core

  1. Overview
  2. Docs
The Coq Proof Assistant -- Core Binaries and Tools

Install 

dune-project
 Dependency

coq.inria.fr Readme Edit opam file Versions (11)

Authors

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

Maintainers

  1. T
    The Coq development team <coqdev@inria.fr>

Sources

coq-8.20.1.tar.gz
md5=0cfaa70f569be9494d24c829e6555d46
sha512=8ee967c636b67b22a4f34115871d8f9b9114df309afc9ddf5f61275251088c6e21f6cf745811df75554d30f4cebb6682f23eeb2e88b771330c4b60ce3f6bf5e2

doc/coq-core.checklib/Coq_checklib/Values/index.html

Module Coq_checklib.ValuesSource

Sourcetype value =
  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 * value array
    (*

    A debug name and sub-values in this block

    *)
  4. | Sum of string * int * value array array
    (*

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

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

    Builtin Ocaml types.

    *)
  10. | Annot of string * value
    (*

    Adds a debug note to the inner value

    *)
  11. | Dyn
    (*

    Coq's Dyn.t

    *)
  12. | Proxy of value ref
    (*

    Same as the inner value, used to define recursive types

    *)
  13. | Int64
  14. | Float64

NB: List and Opt have their own constructors to make it easy to define eg let rec foo = List foo.

Sourceval v_univopaques : value
Sourceval v_libsum : value
Sourceval v_lib : value
Sourceval v_opaquetable : value
Sourceval v_stm_seg : value
Sourceval v_vmlib : value