package coq-core

You can search for identifiers within the package.

in-package search v0.2.0

The Coq Proof Assistant -- Core Binaries and Tools

Install

md5=0cfaa70f569be9494d24c829e6555d46

sha512=8ee967c636b67b22a4f34115871d8f9b9114df309afc9ddf5f61275251088c6e21f6cf745811df75554d30f4cebb6682f23eeb2e88b771330c4b60ce3f6bf5e2

Sourcetype value =

| Any
(*
A value that we won't check,
*)
| Fail of string
(*
A value that shouldn't be there at all,
*)
| Tuple of string * value array
(*
A debug name and sub-values in this block
*)
| 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
*)
| Array of value
| List of value
| Opt of value
| Int
| String
(*
Builtin Ocaml types.
*)
| Annot of string * value
(*
Adds a debug note to the inner value
*)
| Dyn
(*
Coq's Dyn.t
*)
| Proxy of value ref
(*
Same as the inner value, used to define recursive types
*)
| Int64
| 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