package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
Toplevel values
type closure
type valexpr =
  1. | ValInt of int
    (*

    Immediate integers

    *)
  2. | ValBlk of Tac2expr.tag * valexpr array
    (*

    Structured blocks

    *)
  3. | ValStr of Stdlib.Bytes.t
    (*

    Strings

    *)
  4. | ValCls of closure
    (*

    Closures

    *)
  5. | ValOpn of Names.KerName.t * valexpr array
    (*

    Open constructors

    *)
  6. | ValExt : 'a Tac2dyn.Val.tag * 'a -> valexpr
    (*

    Arbitrary data

    *)
  7. | ValUint63 of Uint63.t
    (*

    Primitive integers

    *)
  8. | ValFloat of Float64.t
    (*

    Primitive floats

    *)
type 'a arity
val arity_one : (valexpr -> valexpr Proofview.tactic) arity
val arity_suc : 'a arity -> (valexpr -> 'a) arity
val mk_closure : 'v arity -> 'v -> closure
module Valexpr : sig ... end
Ltac2 FFI
type 'a repr
val repr_of : 'a repr -> 'a -> valexpr
val repr_to : 'a repr -> valexpr -> 'a
val make_repr : ('a -> valexpr) -> (valexpr -> 'a) -> 'a 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.

val of_unit : unit -> valexpr
val to_unit : valexpr -> unit
val unit : unit repr
val of_int : int -> valexpr
val to_int : valexpr -> int
val int : int repr
val of_bool : bool -> valexpr
val to_bool : valexpr -> bool
val bool : bool repr
val of_char : char -> valexpr
val to_char : valexpr -> char
val char : char repr
val of_string : Stdlib.Bytes.t -> valexpr
val to_string : valexpr -> Stdlib.Bytes.t
val string : Stdlib.Bytes.t repr
val of_list : ('a -> valexpr) -> 'a list -> valexpr
val to_list : (valexpr -> 'a) -> valexpr -> 'a list
val list : 'a repr -> 'a list repr
val of_constr : EConstr.t -> valexpr
val to_constr : valexpr -> EConstr.t
val constr : EConstr.t repr
val of_exn : Exninfo.iexn -> valexpr
val to_exn : valexpr -> Exninfo.iexn
val exn : Exninfo.iexn repr
val of_ident : Names.Id.t -> valexpr
val to_ident : valexpr -> Names.Id.t
val ident : Names.Id.t repr
val of_closure : closure -> valexpr
val to_closure : valexpr -> closure
val closure : closure repr
val of_block : (int * valexpr array) -> valexpr
val to_block : valexpr -> int * valexpr array
val block : (int * valexpr array) repr
val of_array : ('a -> valexpr) -> 'a array -> valexpr
val to_array : (valexpr -> 'a) -> valexpr -> 'a array
val array : 'a repr -> 'a array repr
val of_tuple : valexpr array -> valexpr
val to_tuple : valexpr -> valexpr array
val of_pair : ('a -> valexpr) -> ('b -> valexpr) -> ('a * 'b) -> valexpr
val to_pair : (valexpr -> 'a) -> (valexpr -> 'b) -> valexpr -> 'a * 'b
val pair : 'a repr -> 'b repr -> ('a * 'b) repr
val of_option : ('a -> valexpr) -> 'a option -> valexpr
val to_option : (valexpr -> 'a) -> valexpr -> 'a option
val option : 'a repr -> 'a option repr
val of_pattern : Pattern.constr_pattern -> valexpr
val to_pattern : valexpr -> Pattern.constr_pattern
val of_pp : Pp.t -> valexpr
val to_pp : valexpr -> Pp.t
val pp : Pp.t repr
val of_constant : Names.Constant.t -> valexpr
val to_constant : valexpr -> Names.Constant.t
val constant : Names.Constant.t repr
val of_reference : Names.GlobRef.t -> valexpr
val to_reference : valexpr -> Names.GlobRef.t
val reference : Names.GlobRef.t repr
val of_ext : 'a Tac2dyn.Val.tag -> 'a -> valexpr
val to_ext : 'a Tac2dyn.Val.tag -> valexpr -> 'a
val repr_ext : 'a Tac2dyn.Val.tag -> 'a repr
val of_open : (Names.KerName.t * valexpr array) -> valexpr
val to_open : valexpr -> Names.KerName.t * valexpr array
val open_ : (Names.KerName.t * valexpr array) repr
val of_uint63 : Uint63.t -> valexpr
val to_uint63 : valexpr -> Uint63.t
val uint63 : Uint63.t repr
val of_float : Float64.t -> valexpr
val to_float : valexpr -> Float64.t
val float : Float64.t repr
type ('a, 'b) fun1
val app_fun1 : ('a, 'b) fun1 -> 'a repr -> 'b repr -> 'a -> 'b Proofview.tactic
val to_fun1 : 'a repr -> 'b repr -> valexpr -> ('a, 'b) fun1
val fun1 : 'a repr -> 'b repr -> ('a, 'b) fun1 repr
val valexpr : valexpr repr
Dynamic tags
val val_constr : EConstr.t Tac2dyn.Val.tag
val val_ident : Names.Id.t Tac2dyn.Val.tag
val val_pp : Pp.t Tac2dyn.Val.tag
val val_inductive : Names.inductive Tac2dyn.Val.tag
val val_constructor : Names.constructor Tac2dyn.Val.tag
val val_projection : Names.Projection.t Tac2dyn.Val.tag
val val_free : Names.Id.Set.t Tac2dyn.Val.tag

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

Closures

val 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.

val 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.

Exception

exception LtacError of Names.KerName.t * valexpr array

Ltac2-defined exceptions seen from OCaml side

OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct