package rocq-runtime

  1. Overview
  2. Docs
The Rocq Prover -- Core Binaries and Tools

Install 

dune-project
 Dependency

rocq-prover.org Readme Edit opam file Versions (3)

Authors

  1. T
    The Rocq development team, INRIA, CNRS, and contributors

Maintainers

  1. T
    The Rocq development team <rocq+rocq-development@discoursemail.com>

Sources

rocq-9.0.1.tar.gz
sha256=051f7bf702ff0a3b370449728921e5a95e18bc2b31b8eb949d48422888c98af4

doc/ltac2_plugin/Ltac2_plugin/Tac2ffi/index.html

Module Ltac2_plugin.Tac2ffiSource

Ltac2 FFI
Sourcetype 'a repr
Sourceval repr_of : 'a repr -> 'a -> Tac2val.valexpr
Sourceval repr_to : 'a repr -> Tac2val.valexpr -> 'a
Sourceval make_repr : ('a -> Tac2val.valexpr) -> (Tac2val.valexpr -> 'a) -> 'a repr
Sourceval map_repr : ('a -> 'b) -> ('b -> 'a) -> 'a repr -> 'b repr

These functions allow to convert back and forth between OCaml and Ltac2 data representation. The to_* functions raise an anomaly whenever the data has not expected shape.

Sourceval of_unit : unit -> Tac2val.valexpr
Sourceval to_unit : Tac2val.valexpr -> unit
Sourceval unit : unit repr
Sourceval of_int : int -> Tac2val.valexpr
Sourceval to_int : Tac2val.valexpr -> int
Sourceval int : int repr
Sourceval of_bool : bool -> Tac2val.valexpr
Sourceval to_bool : Tac2val.valexpr -> bool
Sourceval bool : bool repr
Sourceval of_char : char -> Tac2val.valexpr
Sourceval to_char : Tac2val.valexpr -> char
Sourceval char : char repr
Sourceval of_bytes : Stdlib.Bytes.t -> Tac2val.valexpr
Sourceval to_bytes : Tac2val.valexpr -> Stdlib.Bytes.t
Sourceval bytes : Stdlib.Bytes.t repr
Sourceval of_string : string -> Tac2val.valexpr

WARNING these functions copy

Sourceval to_string : Tac2val.valexpr -> string
Sourceval string : string repr
Sourceval of_list : ('a -> Tac2val.valexpr) -> 'a list -> Tac2val.valexpr
Sourceval to_list : (Tac2val.valexpr -> 'a) -> Tac2val.valexpr -> 'a list
Sourceval list : 'a repr -> 'a list repr
Sourceval of_constr : EConstr.t -> Tac2val.valexpr
Sourceval to_constr : Tac2val.valexpr -> EConstr.t
Sourceval constr : EConstr.t repr
Sourceval exninfo : Exninfo.info repr
Sourceval of_block : (int * Tac2val.valexpr array) -> Tac2val.valexpr
Sourceval to_block : Tac2val.valexpr -> int * Tac2val.valexpr array
Sourceval block : (int * Tac2val.valexpr array) repr
Sourceval of_array : ('a -> Tac2val.valexpr) -> 'a array -> Tac2val.valexpr
Sourceval to_array : (Tac2val.valexpr -> 'a) -> Tac2val.valexpr -> 'a array
Sourceval array : 'a repr -> 'a array repr
Sourceval of_tuple : Tac2val.valexpr array -> Tac2val.valexpr
Sourceval to_tuple : Tac2val.valexpr -> Tac2val.valexpr array
Sourceval of_pair : ('a -> Tac2val.valexpr) -> ('b -> Tac2val.valexpr) -> ('a * 'b) -> Tac2val.valexpr
Sourceval to_pair : (Tac2val.valexpr -> 'a) -> (Tac2val.valexpr -> 'b) -> Tac2val.valexpr -> 'a * 'b
Sourceval pair : 'a repr -> 'b repr -> ('a * 'b) repr
Sourceval of_triple : ('a -> Tac2val.valexpr) -> ('b -> Tac2val.valexpr) -> ('c -> Tac2val.valexpr) -> ('a * 'b * 'c) -> Tac2val.valexpr
Sourceval to_triple : (Tac2val.valexpr -> 'a) -> (Tac2val.valexpr -> 'b) -> (Tac2val.valexpr -> 'c) -> Tac2val.valexpr -> 'a * 'b * 'c
Sourceval triple : 'a repr -> 'b repr -> 'c repr -> ('a * 'b * 'c) repr
Sourceval of_option : ('a -> Tac2val.valexpr) -> 'a option -> Tac2val.valexpr
Sourceval to_option : (Tac2val.valexpr -> 'a) -> Tac2val.valexpr -> 'a option
Sourceval option : 'a repr -> 'a option repr
Sourceval of_evar : Evar.t -> Tac2val.valexpr
Sourceval to_evar : Tac2val.valexpr -> Evar.t
Sourceval evar : Evar.t repr
Sourceval pp : Pp.t repr
Sourceval reference : Names.GlobRef.t repr
Sourceval of_ext : 'a Tac2dyn.Val.tag -> 'a -> Tac2val.valexpr
Sourceval to_ext : 'a Tac2dyn.Val.tag -> Tac2val.valexpr -> 'a
Sourceval repr_ext : 'a Tac2dyn.Val.tag -> 'a repr
Sourceval open_ : (Names.KerName.t * Tac2val.valexpr array) repr
Sourceval of_uint63 : Uint63.t -> Tac2val.valexpr
Sourceval to_uint63 : Tac2val.valexpr -> Uint63.t
Sourceval uint63 : Uint63.t repr
Sourceval float : Float64.t repr
Sourceval of_pstring : Pstring.t -> Tac2val.valexpr
Sourceval to_pstring : Tac2val.valexpr -> Pstring.t
Sourceval pstring : Pstring.t repr
Sourcetype ('a, 'b) fun1
Sourceval app_fun1 : ('a, 'b) fun1 -> 'a repr -> 'b repr -> 'a -> 'b Proofview.tactic
Sourceval to_fun1 : 'a repr -> 'b repr -> Tac2val.valexpr -> ('a, 'b) fun1
Sourceval fun1 : 'a repr -> 'b repr -> ('a, 'b) fun1 repr
Dynamic tags
Sourceval val_transparent_state : TransparentState.t Tac2dyn.Val.tag

Toplevel representation of OCaml exceptions. Invariant: no LtacError should be put into a value with tag val_exn.

Exception

Sourceexception LtacError of Names.KerName.t * Tac2val.valexpr array

Ltac2-defined exceptions seen from OCaml side