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.1.tar.gz

md5=0cfaa70f569be9494d24c829e6555d46

sha512=8ee967c636b67b22a4f34115871d8f9b9114df309afc9ddf5f61275251088c6e21f6cf745811df75554d30f4cebb6682f23eeb2e88b771330c4b60ce3f6bf5e2

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