package rocq-runtime

  1. Overview
  2. Docs
On This Page
  1. Generic arguments
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 <coqdev@inria.fr>

Sources

rocq-9.0.0.tar.gz
md5=8d522602d23e7a665631826dab9aa92b
sha512=f4f76a6a178e421c99ee7a331a2fd97a06e9c5d0168d7e60c44e3820d8e1a124370ea104ad90c7f87a9a1e9d87b2d0d7d2d387c998feeaed4a75ed04e176a4be

doc/ltac2_plugin/Ltac2_plugin/Tac2quote/index.html

Module Ltac2_plugin.Tac2quoteSource

Syntactic quoting of expressions.

Contrarily to Tac2ffi, which lives on the semantic level, this module manipulates pure syntax of Ltac2. Its main purpose is to write notations.

Sourceval of_pair : ('a -> Tac2expr.raw_tacexpr) -> ('b -> Tac2expr.raw_tacexpr) -> ('a * 'b) CAst.t -> Tac2expr.raw_tacexpr
Sourceval of_constr : ?delimiters:Names.Id.t list -> Constrexpr.constr_expr -> Tac2expr.raw_tacexpr
Sourceval of_open_constr : ?delimiters:Names.Id.t list -> Constrexpr.constr_expr -> Tac2expr.raw_tacexpr
Sourceval of_preterm : ?delimiters:Names.Id.t list -> Constrexpr.constr_expr -> Tac2expr.raw_tacexpr
Sourceval of_list : ?loc:Loc.t -> ('a -> Tac2expr.raw_tacexpr) -> 'a list -> Tac2expr.raw_tacexpr
Sourceval array_literal : ?loc:Loc.t -> Tac2expr.raw_tacexpr list -> Tac2expr.raw_tacexpr

id ↦ 'Control.hyp @id'

Sourceval of_exact_hyp : ?loc:Loc.t -> Names.Id.t CAst.t -> Tac2expr.raw_tacexpr

id ↦ 'Control.refine (fun () => Control.hyp @id')

Sourceval of_exact_var : ?loc:Loc.t -> Names.Id.t CAst.t -> Tac2expr.raw_tacexpr

id ↦ 'Control.refine (fun () => Control.hyp @id')

Generic arguments