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

Dune Dependency

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

Authors

T

The Coq development team, INRIA, CNRS, and contributors

Maintainers

T

The Coq development team <coqdev@inria.fr>

Sources

coq-8.20.0.tar.gz

md5=66e57ea55275903bef74d5bf36fbe0f1

sha512=1a7eac6e2f58724a3f9d68bbb321e4cfe963ba1a5551b9b011db4b3f559c79be433d810ff262593d753770ee41ea68fbd6a60daa1e2319ea00dff64c8851d70b

doc/ltac2_plugin/Ltac2_plugin/Tac2val/index.html

Module `Ltac2_plugin.Tac2val`Source

Toplevel values

Dynamic semantics

Values are represented in a way similar to OCaml, i.e. they contrast immediate integers (integers, constructors without arguments) and structured blocks (tuples, arrays, constructors with arguments), as well as a few other base cases, namely closures, strings, named constructors, and dynamic type coming from the Coq implementation.

Sourcetype tag = int

Sourcetype closure

Sourcetype valexpr =

| ValInt of int
(*
Immediate integers
*)
| ValBlk of tag * valexpr array
(*
Structured blocks
*)
| ValStr of Stdlib.Bytes.t
(*
Strings
*)
| ValCls of closure
(*
Closures
*)
| ValOpn of Names.KerName.t * valexpr array
(*
Open constructors
*)
| ValExt : 'a Tac2dyn.Val.tag * 'a -> valexpr
(*
Arbitrary data
*)

Sourcemodule Valexpr : sig ... end

Closures

Sourcetype 'a arity

Sourceval arity_one : (valexpr -> valexpr Proofview.tactic) arity

Sourceval arity_suc : 'a arity -> (valexpr -> 'a) arity

Sourceval mk_closure : 'v arity -> 'v -> closure

Sourceval mk_closure_val : 'v arity -> 'v -> valexpr

Composition of mk_closure and ValCls

Sourceval annotate_closure : Tac2expr.frame -> closure -> closure

The closure must not be already annotated

Sourceval to_closure : valexpr -> closure

Sourceval apply : closure -> valexpr list -> valexpr Proofview.tactic

Given a closure, apply it to some arguments. Handling of argument mismatches is done automatically, i.e. in case of over or under-application.

Sourceval apply_val : valexpr -> valexpr list -> valexpr Proofview.tactic

Composition of to_closure and apply

Sourceval abstract : int -> (valexpr list -> valexpr Proofview.tactic) -> closure

Turn a fixed-arity function into a closure. The inner function is guaranteed to be applied to a list whose size is the integer argument.

On This Page

Toplevel values
Dynamic semantics