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 <rocq+rocq-development@discoursemail.com>

Sources

rocq-9.1.0.tar.gz
sha256=b236dc44f92e1eeca6877c7ee188a90c2303497fe7beb99df711ed5a7ce0d824

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