package rocq-runtime
Install
Dune Dependency
Authors
Maintainers
Sources
md5=8d522602d23e7a665631826dab9aa92b
sha512=f4f76a6a178e421c99ee7a331a2fd97a06e9c5d0168d7e60c44e3820d8e1a124370ea104ad90c7f87a9a1e9d87b2d0d7d2d387c998feeaed4a75ed04e176a4be
doc/ltac2_plugin/Ltac2_plugin/Tac2val/index.html
Module Ltac2_plugin.Tac2valSource
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 Rocq implementation.
type 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
*)
Closures
The arrows in 'v should be pure. Use tclLIFT or do tclUNIT () >>= fun () -> f args when you need effects.
The closure must not be already annotated
For internal use (Tac2externals). Wraps the applications of the 'v argument to make it pure.
Given a closure, apply it to some arguments. Handling of argument mismatches is done automatically, i.e. in case of over or under-application.
Composition of to_closure and apply
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.