package rocq-runtime

You can search for identifiers within the package.

in-package search v0.2.0

The Rocq Prover -- Core Binaries and Tools

Install

dune-project

Dependency

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

Authors

T

The Rocq development team, INRIA, CNRS, and contributors

Maintainers

T

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

Sources

rocq-9.1.0.tar.gz

sha256=b236dc44f92e1eeca6877c7ee188a90c2303497fe7beb99df711ed5a7ce0d824

doc/funind_plugin/Funind_plugin/Glob_term_to_relation/index.html

Module `Funind_plugin.Glob_term_to_relation`Source

Source

val build_inductive : 
  Evd.evar_map ->
  Constr.pconstant list ->
  (Names.Name.t * Glob_term.glob_constr * Glob_term.glob_constr option) list
    list ->
  Constrexpr.constr_expr list ->
  Glob_term.glob_constr list ->
  unit

package rocq-runtime

Install

dune-project Dependency

Authors

Maintainers

Sources

doc/funind_plugin/Funind_plugin/Glob_term_to_relation/index.html

Module Funind_plugin.Glob_term_to_relationSource

dune-project
Dependency

Module `Funind_plugin.Glob_term_to_relation`Source