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=66e57ea55275903bef74d5bf36fbe0f1

sha512=1a7eac6e2f58724a3f9d68bbb321e4cfe963ba1a5551b9b011db4b3f559c79be433d810ff262593d753770ee41ea68fbd6a60daa1e2319ea00dff64c8851d70b

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